diff --git a/coq/CPS.v b/coq/CPS.v
index b5f4352b..1c6ed129 100644
--- a/coq/CPS.v
+++ b/coq/CPS.v
@@ -211,13 +211,13 @@ Section CPS.
                        k (Some (l, (sigma fn) v, Gamma))
                      | None => k None
                      end)
-      | InternalCall fn args body =>
+      | InternalCall fn args =>
         fun k =>
           interp_args'_cps (@cps) args
                            (fun res =>
                               match res with
                               | Some (l, argvals, Gamma) =>
-                                cps body (fun res =>
+                                cps fn.(int_body) (fun res =>
                                             match res with
                                             | Some (l, v, _) =>
                                               k (Some (l, v, Gamma))
diff --git a/coq/CompactSemantics.v b/coq/CompactSemantics.v
index 84646f79..e94c7e25 100644
--- a/coq/CompactSemantics.v
+++ b/coq/CompactSemantics.v
@@ -133,9 +133,9 @@ Section Interp.
       | ExternalCall fn arg1 => fun Gamma =>
         let/opt3 action_log, arg1, Gamma := interp_action Gamma sched_log action_log arg1 in
         Some (action_log, sigma fn arg1, Gamma)
-      | InternalCall name args body => fun Gamma =>
+      | InternalCall fn args => fun Gamma =>
         let/opt3 action_log, results, Gamma := interp_args' (@interp_action) Gamma sched_log action_log args in
-        let/opt3 action_log, v, _ := interp_action results sched_log action_log body in
+        let/opt3 action_log, v, _ := interp_action results sched_log action_log fn.(int_body) in
         Some (action_log, v, Gamma)
       | APos _ a => fun Gamma =>
         interp_action Gamma sched_log action_log a
diff --git a/coq/Desugaring.v b/coq/Desugaring.v
index a8238c60..4f80331a 100644
--- a/coq/Desugaring.v
+++ b/coq/Desugaring.v
@@ -33,7 +33,7 @@ Section Desugaring.
     | UBinop fn arg1 arg2 => UBinop fn (d arg1) (d arg2)
     | UExternalCall fn arg => UExternalCall (fSigma fn) (d arg)
     | UInternalCall fn args =>
-      UInternalCall (map_intf_body d fn) (List.map d args)
+      UInternalCall (map_uintf_body d fn) (List.map d args)
     | UAPos p e => UAPos p (d e)
     | USugar s => desugar pos fR fSigma s
     end
@@ -77,7 +77,7 @@ Section Desugaring.
            SyntaxMacros.uswitch (d var) (d default) branches
          | UCallModule fR' fSigma' fn args =>
            let df body := desugar_action' pos (fun r => fR (fR' r)) (fun fn => fSigma (fSigma' fn)) body in
-           UInternalCall (map_intf_body df fn) (List.map d args)
+           UInternalCall (map_uintf_body df fn) (List.map d args)
          end.
 
   Definition desugar_action (pos: pos_t) (a: uaction reg_t ext_fn_t)
diff --git a/coq/Frontend.v b/coq/Frontend.v
index 5e7ebcca..d99b063b 100644
--- a/coq/Frontend.v
+++ b/coq/Frontend.v
@@ -80,8 +80,8 @@ Notation rule := (rule pos_t var_t fn_name_t).
 
 Notation scheduler := (scheduler pos_t _).
 
-Notation UInternalFunction reg_t ext_fn_t := (InternalFunction var_t fn_name_t (uaction reg_t ext_fn_t)).
-Notation InternalFunction R Sigma sig tau := (InternalFunction var_t fn_name_t (action R Sigma sig tau)).
+Notation UInternalFunction reg_t ext_fn_t := (UInternalFunction pos_t var_t fn_name_t reg_t ext_fn_t).
+Notation InternalFunction R Sigma sig tau := (InternalFunction pos_t var_t fn_name_t R Sigma sig tau).
 
 Notation register_update_circuitry R Sigma := (register_update_circuitry _ R Sigma ContextEnv).
 
@@ -213,7 +213,7 @@ Notation tc_rule R Sigma ua :=
   (tc_action R Sigma (@List.nil (var_t * type)) unit_t ua) (only parsing).
 
 Notation tc_function R Sigma uf :=
-  (tc_action R Sigma (int_argspec uf) (int_retSig uf) (int_body uf)) (only parsing).
+  (tc_action R Sigma (uint_argspec uf) (uint_retType uf) (uint_body uf)) (only parsing).
 
 Ltac _arg_type R :=
   match type of R with
diff --git a/coq/Lowering.v b/coq/Lowering.v
index 9db55922..d931fe8d 100644
--- a/coq/Lowering.v
+++ b/coq/Lowering.v
@@ -130,10 +130,10 @@ Section Lowering.
         lower_binop fn (l a1) (l a2)
       | TypedSyntax.ExternalCall fn a =>
         LoweredSyntax.ExternalCall fn (l a)
-      | TypedSyntax.InternalCall fn args body =>
+      | TypedSyntax.InternalCall fn args =>
         SyntaxMacros.InternalCall
           (lower_args' (@lower_action) args)
-          (l body)
+          (l fn.(int_body))
       | TypedSyntax.APos p a =>
         LoweredSyntax.APos p (l a)
       end.
diff --git a/coq/Parsing.v b/coq/Parsing.v
index 0ddf20af..4217b5c2 100644
--- a/coq/Parsing.v
+++ b/coq/Parsing.v
@@ -131,17 +131,11 @@ Notation "a '[' b ':+' c ']'" := (UBinop (UBits2 (UIndexedSlice c)) a b) (in cus
 Notation "'`' a '`'" := ( a) (in custom koika at level 99, a constr at level 99).
 
 Notation "'fun' nm args ':' ret '=>' body" :=
-  {| int_name := nm%string;
-     int_argspec := args;
-     int_retSig := ret;
-     int_body := body |}
-    (in custom koika at level 99, nm custom koika_var at level 0, args custom koika_types, ret constr at level 0, body custom koika at level 99, format "'[v' 'fun'  nm  args  ':'  ret  '=>' '/' body ']'").
+  (Build_UInternalFunction' nm%string args ret body)
+    (in custom koika at level 99, nm custom koika_var at level 0, args custom koika_types, ret constr at level 0, body custom koika at level 99, right associativity, format "'[v' 'fun'  nm  args  ':'  ret  '=>' '/' body ']'").
 Notation "'fun' nm '()' ':' ret '=>' body" :=
-  {| int_name := nm%string;
-     int_argspec := nil;
-     int_retSig := ret;
-     int_body := body |}
-    (in custom koika at level 99, nm custom koika_var at level 0, ret constr at level 0, body custom koika at level 99, format "'[v' 'fun'  nm  '()'   ':'  ret  '=>' '/' body ']'").
+  (Build_UInternalFunction' nm%string nil ret body)
+    (in custom koika at level 99, nm custom koika_var at level 0, ret constr at level 0, body custom koika at level 99, right associativity, format "'[v' 'fun'  nm  '()'   ':'  ret  '=>' '/' body ']'").
 
 (* Deprecated *)
 Notation "'call' instance method args" :=
@@ -268,10 +262,6 @@ Module Type Tests.
   (* Notation "'{&' a '&}'" := (a) (a custom koika_types at level 200). *)
   (* Definition test_21 := {& "yoyo" : bits_t 2 &}. *)
   (* Definition test_22 := {& "yoyo" : bits_t 2 , "yoyo" : bits_t 2  &}. *)
-  Definition test_23 : InternalFunction string string (uaction reg_t) := {{ fun test (arg1 : (bits_t 3)) (arg2 : bits_t 2) : bits_t 4 => magic }}.
-  Definition test_24 : nat -> InternalFunction string string (uaction reg_t) :=  (fun sz => {{ fun test (arg1 : bits_t sz) (arg1 : bits_t sz) : bits_t sz  => magic}}).
-  Definition test_25 : nat -> InternalFunction string string (uaction reg_t) := (fun sz => {{fun test (arg1 : bits_t sz ) : bits_t sz => let oo := magic >> magic in magic}}).
-  Definition test_26 : nat -> InternalFunction string string (uaction reg_t) := (fun sz => {{ fun test () : bits_t sz  => magic }}).
   Definition test_27 : uaction reg_t :=
     {{
         (if (!read0(data0)) then
@@ -283,6 +273,12 @@ Module Type Tests.
            read0(data0));
         fail
     }}.
+  Notation UInternalFunction :=
+    (UInternalFunction pos_t string string reg_t ext_fn_t).
+  Definition test_23 : UInternalFunction := {{ fun test (arg1 : (bits_t 3)) (arg2 : bits_t 2) : bits_t 4 => magic }}.
+  Definition test_24 : nat -> UInternalFunction :=  (fun sz => {{ fun test (arg1 : bits_t sz) (arg1 : bits_t sz) : bits_t sz  => magic}}).
+  Definition test_25 : nat -> UInternalFunction := (fun sz => {{fun test (arg1 : bits_t sz ) : bits_t sz => let oo := magic >> magic in magic}}).
+  Definition test_26 : nat -> UInternalFunction := (fun sz => {{ fun test () : bits_t sz  => magic }}).
   Definition test_28 : uaction reg_t :=  {{
                                              match var with
                                              | magic => magic
diff --git a/coq/Syntax.v b/coq/Syntax.v
index c44b4d87..c0f9f070 100644
--- a/coq/Syntax.v
+++ b/coq/Syntax.v
@@ -20,7 +20,7 @@ Section Syntax.
   | UUnop (ufn1: PrimUntyped.ufn1) (arg1: uaction)
   | UBinop (ufn2: PrimUntyped.ufn2) (arg1: uaction) (arg2: uaction)
   | UExternalCall (ufn: ext_fn_t) (arg: uaction)
-  | UInternalCall (ufn: InternalFunction var_t fn_name_t uaction) (args: list uaction)
+  | UInternalCall (ufn: UInternalFunction' var_t fn_name_t uaction) (args: list uaction)
   | UAPos (p: pos_t) (e: uaction)
   | USugar (s: usugar)
   with usugar {reg_t ext_fn_t} :=
@@ -40,7 +40,7 @@ Section Syntax.
   | UCallModule {module_reg_t module_ext_fn_t: Type}
                 (fR: module_reg_t -> reg_t)
                 (fSigma: @Lift module_ext_fn_t ext_fn_t)
-                (fn: InternalFunction var_t fn_name_t (@uaction module_reg_t module_ext_fn_t))
+                (fn: UInternalFunction' var_t fn_name_t (@uaction module_reg_t module_ext_fn_t))
                 (args: list uaction).
 
   Inductive scheduler :=
@@ -54,3 +54,8 @@ Arguments Lift: clear implicits.
 Arguments usugar : clear implicits.
 Arguments uaction : clear implicits.
 Arguments scheduler : clear implicits.
+
+Notation UInternalFunction pos_t var_t fn_name_t reg_t ext_fn_t :=
+  (UInternalFunction'
+     var_t fn_name_t
+     (uaction pos_t var_t fn_name_t reg_t ext_fn_t)).
diff --git a/coq/SyntaxFunctions.v b/coq/SyntaxFunctions.v
index a64065ba..a52c330c 100644
--- a/coq/SyntaxFunctions.v
+++ b/coq/SyntaxFunctions.v
@@ -40,7 +40,7 @@ Section SyntaxFunctions.
         | UExternalCall ufn arg =>
           UExternalCall ufn (r 0 arg)
         | UInternalCall ufn arg =>
-          let ufn := map_intf_body (r 0) ufn in
+          let ufn := map_uintf_body (r 0) ufn in
           let args := snd (foldi (fun n a args => (r n a :: args)) 1 [] arg) in
           UInternalCall ufn args
         | UAPos _ e => (r 0 e)
@@ -78,7 +78,7 @@ Section SyntaxFunctions.
                  foldi (fun n a elements => (r n a) :: elements) 0 [] elements in
              UArrayInit tau elements
            | UCallModule fR fSigma ufn args =>
-             let ufn := map_intf_body (r 0) ufn in
+             let ufn := map_uintf_body (r 0) ufn in
              let args := snd (foldi (fun n a args => (r n a :: args)) 1 [] args) in
              UCallModule fR fSigma ufn args
            end.
@@ -154,11 +154,11 @@ Section SyntaxFunctions.
               let '(f, arg) := pe 0 arg in
               (f, UExternalCall ufn arg)
             | UInternalCall ufn args =>
-              let '(fbody, body) := pe 0 ufn.(int_body) in
+              let '(fbody, body) := pe 0 ufn.(uint_body) in
               let ufn :=
                   if fbody then
                     (* Only unfold the body if the error is in it *)
-                    map_intf_body (fun _ => body) ufn
+                    map_uintf_body (fun _ => body) ufn
                   else ufn in
               let '(n, (fargs, args)) :=
                   foldi (fun n arg '(fargs, args) =>
@@ -228,10 +228,10 @@ Section SyntaxFunctions.
                        0 ([], []) fields in
              (ffields, UStructInit sig fields)
            | UCallModule fR fSigma ufn args =>
-              let '(fbody, body) := pe 0 ufn.(int_body) in
+              let '(fbody, body) := pe 0 ufn.(uint_body) in
               let ufn :=
                   if fbody then (* Only unfold the body if the error is in it *)
-                    map_intf_body (fun _ => body) ufn
+                    map_uintf_body (fun _ => body) ufn
                   else ufn in
               let '(n, (fargs, args)) :=
                   foldi (fun n arg '(fargs, args) =>
@@ -267,7 +267,7 @@ Section SyntaxFunctions.
            | UInternalCall ufn args =>
              List.fold_left
                (fun acc arg => acc + uaction_size arg)
-               args (uaction_size ufn.(int_body))
+               args (uaction_size ufn.(uint_body))
            | UAPos p e => uaction_size e
            | USugar s => usugar_size s
            | _ => 0
@@ -301,7 +301,7 @@ Section SyntaxFunctions.
                 | UCallModule fR fSigma fn args =>
                   List.fold_left
                     (fun acc arg => acc + uaction_size arg)
-                    args (uaction_size fn.(int_body))
+                    args (uaction_size fn.(uint_body))
                 | _ => 0
                 end)%N.
   End TermSize.
diff --git a/coq/SyntaxMacros.v b/coq/SyntaxMacros.v
index 112bebd4..e1f407ac 100644
--- a/coq/SyntaxMacros.v
+++ b/coq/SyntaxMacros.v
@@ -146,47 +146,44 @@ Module Display.
     Context {pos_t reg_t ext_fn_t: Type}.
 
     Notation uaction := (uaction pos_t var_t fn_name_t reg_t ext_fn_t).
+    Notation intfun := (UInternalFunction pos_t var_t fn_name_t reg_t ext_fn_t).
 
     Inductive field : Type :=
     | Str (s: string)
     | Value (tau: type).
 
-    Notation intfun := (InternalFunction var_t fn_name_t uaction).
-
-    Definition empty_printer : InternalFunction var_t fn_name_t uaction :=
-      {| int_name := "print";
-         int_argspec := [];
-         int_retSig := unit_t;
-         int_body := USugar USkip |}.
+    Definition empty_printer : intfun :=
+      {| uint_name := "print";
+         uint_argspec := [];
+         uint_retType := unit_t;
+         uint_body := USugar USkip |}.
 
     Definition display_utf8 s : uaction :=
       UUnop (UDisplay (UDisplayUtf8)) (USugar (UConstString s)).
 
-    Definition nl_printer : InternalFunction var_t fn_name_t uaction :=
-      {| int_name := "print_nl";
-         int_argspec := [];
-         int_retSig := unit_t;
-         int_body := display_utf8 "\n" |}.
+    Definition nl_printer : intfun :=
+      {| uint_name := "print_nl";
+         uint_argspec := [];
+         uint_retType := unit_t;
+         uint_body := display_utf8 "\n" |}.
 
     Definition extend_printer f (offset: nat) (printer: intfun) : intfun :=
       let opts :=
           {| display_newline := false; display_strings := false; display_style := dFull |} in
       let display_value arg :=
           UUnop (UDisplay (UDisplayValue opts)) (UVar arg) in
-      let '(Build_InternalFunction int_name int_argspec int_retSig int_body) :=
-          printer in
       match f with
       | Str s =>
-        {| int_name := int_name;
-           int_argspec := int_argspec;
-           int_retSig := int_retSig;
-           int_body := (USeq (display_utf8 s) int_body) |}
+        {| uint_name    := printer.(uint_name);
+           uint_argspec := printer.(uint_argspec);
+           uint_retType  := printer.(uint_retType);
+           uint_body    := (USeq (display_utf8 s) printer.(uint_body)) |}
       | Value tau =>
         let arg := String.append "arg" (show offset) in
-        {| int_name := int_name;
-           int_argspec := (arg, tau) :: int_argspec;
-           int_retSig := unit_t;
-           int_body := (USeq (display_value arg) int_body) |}
+        {| uint_name    := printer.(uint_name);
+           uint_argspec := (arg, tau) :: printer.(uint_argspec);
+           uint_retType  := unit_t;
+           uint_body    := (USeq (display_value arg) printer.(uint_body)) |}
       end.
 
     Fixpoint make_printer (offset: nat) (fstring: list field) : intfun :=
diff --git a/coq/TypeInference.v b/coq/TypeInference.v
index 7c4f474c..b9cc650c 100644
--- a/coq/TypeInference.v
+++ b/coq/TypeInference.v
@@ -146,12 +146,15 @@ Section TypeInference.
         let/res tc_args := result_list_map (type_action pos sig) args in
         let arg_positions := List.map (actpos pos) args in
         let tc_args_w_pos := List.combine arg_positions tc_args in
-        let/res args_ctx := assert_argtypes e fn.(int_name) pos (List.rev fn.(int_argspec)) (List.rev tc_args_w_pos) in
+        let/res args_ctx := assert_argtypes e fn.(uint_name) pos (List.rev fn.(uint_argspec)) (List.rev tc_args_w_pos) in
 
-        let/res fn_body' := type_action (actpos pos fn.(int_body)) (List.rev fn.(int_argspec)) fn.(int_body) in
-        let/res fn_body' := cast_action (actpos pos fn.(int_body)) fn.(int_retSig) (``fn_body') in
+        let/res fn_body' := type_action (actpos pos fn.(uint_body)) (List.rev fn.(uint_argspec)) fn.(uint_body) in
+        let/res fn_body' := cast_action (actpos pos fn.(uint_body)) fn.(uint_retType) (``fn_body') in
 
-        Success (EX (TypedSyntax.InternalCall fn.(int_name) args_ctx fn_body'))
+        Success (EX (TypedSyntax.InternalCall {|
+          int_name := fn.(uint_name);
+          int_body := fn_body';
+        |} args_ctx))
       | UUnop fn arg1 =>
         let pos1 := actpos pos arg1 in
         let/res arg1' := type_action pos sig arg1 in
diff --git a/coq/TypedParsing.v b/coq/TypedParsing.v
index 561fe184..45495fc2 100644
--- a/coq/TypedParsing.v
+++ b/coq/TypedParsing.v
@@ -42,7 +42,7 @@ Definition function
   {tau sig reg_t ext_fn_t}
   (R : reg_t -> type)
   (Sigma: ext_fn_t -> ExternalSignature) :=
-    Types.InternalFunction var_t fn_name_t
+    Types.InternalFunction' fn_name_t
       (TypedSyntax.action pos_t var_t fn_name_t R Sigma sig tau).
 
 Notation "'<{' e '}>'" := (e) (e custom koika_t at level 200).
@@ -199,17 +199,31 @@ Declare Custom Entry koika_t_types_binder.
 Notation "'(' x ':' y ')'" := (x%string, (y : type)) (in custom koika_t_types_binder at level 60, x custom koika_t_var at level 0, y constr at level 12 ).
 Notation "a  ..  b" := (cons a ..  (cons b nil) ..)  (in custom koika_t_types at level 95, a custom koika_t_types_binder , b custom koika_t_types_binder, right associativity).
 
+(* We want to tell the typechecker that the body of the function
+ * should have the function's arguments in its context (sig).
+ *
+ * However, using a type hint where R Sigma are kept implicit
+ * like:
+ * ```
+ * Definition some_act : action R Sigma :=
+ * <{ ... }>: action' (sig := ...) _ _.
+ * ```
+ * does not work since coq is then trying to infer R and Sigma from
+ * the body term instead of the outer definition.
+ *
+ * To tell coq to infer it from the definition we need
+ * bidirectionality hints and thus we need a seperate function.
+ *)
+Local Definition refine_sig_tau sig tau {reg_t ext_fn_t}
+  {R : reg_t -> type} {Sigma : ext_fn_t -> ExternalSignature}
+  (a : action' R Sigma (tau := tau) (sig := sig)) : action' R Sigma := a.
+Arguments refine_sig_tau sig tau {reg_t ext_fn_t} {R Sigma} & a : assert.
+
 Notation "'fun' nm args ':' ret '=>' body" :=
-  ({| int_name := nm%string;
-     int_argspec := args;
-     int_retSig := ret;
-     int_body := body |} : function (sig := args) _ _)
+  (Build_InternalFunction' nm%string (refine_sig_tau args ret body))
     (in custom koika_t at level 99, nm custom koika_t_var at level 0, args custom koika_t_types, ret constr at level 0, body custom koika_t at level 99, format "'[v' 'fun'  nm  args  ':'  ret  '=>' '/' body ']'").
 Notation "'fun' nm '()' ':' ret '=>' body" :=
-  ({| int_name := nm%string;
-     int_argspec := nil;
-     int_retSig := ret;
-     int_body := body |} : function (sig := nil) _ _)
+  (Build_InternalFunction' nm%string (refine_sig_tau nil ret body))
     (in custom koika_t at level 99, nm custom koika_t_var at level 0, ret constr at level 0, body custom koika_t at level 99, format "'[v' 'fun'  nm  '()'   ':'  ret  '=>' '/' body ']'").
 
 (* Koika_args *)
@@ -261,24 +275,28 @@ Fixpoint lift_reg
     | Unop fn arg => Unop fn (lift_reg lift arg)
     | Binop fn arg1 arg2 => Binop fn (lift_reg lift arg1) (lift_reg lift arg2)
     | ExternalCall fn arg => ExternalCall fn (lift_reg lift arg)
-    | InternalCall fn args body =>
-      InternalCall fn (rew List.map_id _ in
+    | InternalCall fn args =>
+      InternalCall {| int_name := fn.(int_name);
+        int_body := (lift_reg lift fn.(int_body)) |}
+      (rew List.map_id _ in
       @cmap _ _ _ (fun k_tau => action' (tau := (snd k_tau)) sR Sigma)
-        id (fun _ => lift_reg lift) _ args) (lift_reg lift body)
+        id (fun _ => lift_reg lift) _ args)
     | APos pos a => APos pos (lift_reg lift a)
     end.
 
-
 Notation "fn args" :=
-  (InternalCall (tau := fn.(int_retSig)) (argspec := rev fn.(int_argspec)) fn.(int_name) args fn.(int_body))
+  (InternalCall fn args)
     (in custom koika_t at level 1, fn constr at level 0 , args custom koika_t_args at level 99, only parsing).
 
 Notation "instance  '.(' fn ')' args" :=
-  (InternalCall (tau := fn.(int_retSig)) (argspec := rev fn.(int_argspec)) fn.(int_name) args (lift_reg (exist _ instance (fun _ => eq_refl)) fn.(int_body)))
+  (InternalCall {|
+    int_name := fn.(int_name);
+    int_body := (lift_reg (exist _ instance (fun _ => eq_refl)) fn.(int_body))
+    |} args)
     (in custom koika_t at level 1, instance constr at level 0, fn constr, args custom koika_t_args at level 99).
 
 Notation "'{' fn '}' args" :=
-  (InternalCall (tau := fn.(int_retSig)) (argspec := rev fn.(int_argspec)) fn.(int_name) args fn.(int_body))
+  (InternalCall fn args)
     (in custom koika_t at level 1, fn constr at level 200 , args custom koika_t_args at level 99, only parsing).
 
 Notation "'extcall' method '(' arg ')'" := (ExternalCall method arg) (in custom koika_t at level 98, method constr at level 0, arg custom koika_t).
@@ -538,7 +556,7 @@ Module Type Tests2.
   Program Definition test_lit : _action (tau := bits_t 5) := (Seq (Write P0 data0 <{ Ob~1~1~0~0~1 }>) (Const (tau := bits_t _) (Bits.of_N ltac:(let x := eval cbv in ((len "01100") * 1) in exact x) (bin_string_to_N "01100")))).
   Fail Next Obligation.
   Definition test_20 : _action := <{ |0b"11001100"| [ Ob~0~0~0 :+ 3 ] }>.
-  Definition test_23 : function R Sigma := <{ fun test (arg1 : (bits_t 3)) (arg2 : bits_t 2) : bits_t 4 => pass }>.
+  Definition test_23 : function R Sigma := <{ fun test (arg1 : (bits_t 3)) (arg2 : bits_t 2) : unit_t => pass }>.
   Definition test_24 (sz : nat) : function R Sigma := <{ fun test (arg1 : bits_t sz) (arg1 : bits_t sz) : bits_t sz  => fail(sz)}>.
   Definition test_25 (sz : nat) : function R Sigma := <{fun test (arg1 : bits_t sz ) : bits_t sz => let oo := fail(sz) >> fail(sz) in oo}>.
   Definition test_26 (sz : nat) : function R Sigma := <{ fun test () : bits_t sz  => fail(sz) }>.
@@ -728,4 +746,4 @@ Module Type Tests2.
   Definition num_test_constr_2 := |0b"0110"|     : bits _.
   Definition num_test_constr_3 := |"c0ffee":h|   : bits _.
   Definition num_test_constr_4 := |0x"deadbeef"| : bits _.
-End Tests2.
\ No newline at end of file
+End Tests2.
diff --git a/coq/TypedSemantics.v b/coq/TypedSemantics.v
index 14a33e6f..65c3c370 100644
--- a/coq/TypedSemantics.v
+++ b/coq/TypedSemantics.v
@@ -110,9 +110,9 @@ Section Interp.
       | ExternalCall fn arg1 => fun Gamma =>
         let/opt3 action_log, arg1, Gamma := interp_action Gamma sched_log action_log arg1 in
         Some (action_log, sigma fn arg1, Gamma)
-      | InternalCall name args body => fun Gamma =>
+      | InternalCall fn args => fun Gamma =>
         let/opt3 action_log, results, Gamma := interp_args' (@interp_action) Gamma sched_log action_log args in
-        let/opt3 action_log, v, _ := interp_action results sched_log action_log body in
+        let/opt3 action_log, v, _ := interp_action results sched_log action_log fn.(int_body) in
         Some (action_log, v, Gamma)
       | APos _ a => fun Gamma =>
         interp_action Gamma sched_log action_log a
diff --git a/coq/TypedSyntax.v b/coq/TypedSyntax.v
index 7451ce76..b3b55692 100644
--- a/coq/TypedSyntax.v
+++ b/coq/TypedSyntax.v
@@ -46,10 +46,10 @@ Section Syntax.
                  (arg: action sig (arg1Sig (Sigma fn)))
     : action sig (retSig (Sigma fn))
   | InternalCall {sig tau}
-                 (fn : fn_name_t)
+                 (* TODO -- why does this list need to be reversed?? *)
                  {argspec : tsig var_t}
-                 (args: context (fun k_tau => action sig (snd k_tau)) (List.rev argspec))
-                 (body : action (List.rev argspec) tau)
+                 (fn : InternalFunction' fn_name_t (action argspec tau))
+                 (args: context (fun k_tau => action sig (snd k_tau)) argspec)
     : action sig tau
   | APos {sig tau} (pos: pos_t) (a: action sig tau)
     : action sig tau.
@@ -59,3 +59,6 @@ End Syntax.
 
 Arguments action pos_t var_t fn_name_t {reg_t ext_fn_t} R Sigma sig tau : assert.
 Arguments rule pos_t var_t fn_name_t {reg_t ext_fn_t} R Sigma : assert.
+
+Notation InternalFunction pos_t var_t fn_name_t R Sigma sig tau :=
+  (InternalFunction' fn_name_t (action pos_t var_t fn_name_t R Sigma sig tau)).
diff --git a/coq/TypedSyntaxFunctions.v b/coq/TypedSyntaxFunctions.v
index cae779af..ca6b647f 100644
--- a/coq/TypedSyntaxFunctions.v
+++ b/coq/TypedSyntaxFunctions.v
@@ -44,9 +44,9 @@ Section TypedSyntaxFunctions.
       | Unop fn arg1 => action_footprint' acc arg1
       | Binop fn arg1 arg2 => action_footprint' (action_footprint' acc arg1) arg2
       | ExternalCall fn arg => action_footprint' acc arg
-      | InternalCall fn args body =>
+      | InternalCall fn args =>
         let acc := cfoldr (fun _ _ arg acc => action_footprint' acc arg) args acc in
-        action_footprint' acc body
+        action_footprint' acc fn.(int_body)
       | APos _ a => action_footprint' acc a
       end.
 
@@ -255,7 +255,7 @@ Section TypedSyntaxFunctions.
       | ExternalCall fn arg =>
         let '(env, arg) := annotate_action_register_histories env arg in
         (env, ExternalCall fn arg)
-      | InternalCall fn args body =>
+      | InternalCall fn args =>
         let '(env, args) :=
             cfoldr (fun sg k arg cont =>
                       fun env =>
@@ -263,8 +263,8 @@ Section TypedSyntaxFunctions.
                         let '(env, args) := cont env in
                         (env, CtxCons k arg args)) args
                    (fun env => (env, CtxEmpty)) env in
-        let '(env, body) := annotate_action_register_histories env body in
-        (env, InternalCall fn args body)
+        let '(env, body) := annotate_action_register_histories env fn.(int_body) in
+        (env, InternalCall {| int_name := fn.(int_name); int_body := body |} args)
       | APos pos a =>
         let '(env, a) := annotate_action_register_histories env a in
         (env, APos (PosAnnot pos) a)
@@ -393,9 +393,9 @@ Section TypedSyntaxFunctions.
       | Unop fn arg1 => rule_max_log_size arg1
       | Binop fn arg1 arg2 => rule_max_log_size arg1 + rule_max_log_size arg2
       | ExternalCall fn arg => rule_max_log_size arg
-      | InternalCall fn args body =>
+      | InternalCall fn args =>
         cfoldl (fun k arg acc => acc + rule_max_log_size arg) args 0
-        + rule_max_log_size body
+        + rule_max_log_size fn.(int_body)
       | APos pos a => rule_max_log_size a
       end.
   End StaticAnalysis.
@@ -418,9 +418,9 @@ Section TypedSyntaxFunctions.
       | Unop fn a => existsb_subterm f a
       | Binop fn a1 a2 => existsb_subterm f a1 || existsb_subterm f a2
       | ExternalCall fn arg => existsb_subterm f arg
-      | InternalCall fn args body =>
+      | InternalCall fn args =>
         cfoldl (fun k arg acc => acc || existsb_subterm f arg) args false
-        || existsb_subterm f body
+        || existsb_subterm f fn.(int_body)
       | APos _ a => existsb_subterm f a
       end.
 
@@ -457,9 +457,9 @@ Section TypedSyntaxFunctions.
     | Unop fn arg1 => is_pure arg1
     | Binop fn arg1 arg2 => is_pure arg1 && is_pure arg2
     | ExternalCall fn arg => false
-    | InternalCall fn args body =>
+    | InternalCall fn args =>
       cfoldr (fun _ k arg acc => acc && is_pure arg) args true
-      && is_pure body
+      && is_pure fn.(int_body)
     | APos pos a => is_pure a
     end.
 
@@ -477,7 +477,7 @@ Section TypedSyntaxFunctions.
     | Unop fn arg1 => false
     | Binop fn arg1 arg2 => false
     | ExternalCall fn arg => false
-    | InternalCall fn args body => returns_zero body
+    | InternalCall fn args => returns_zero fn.(int_body)
     | APos pos a => returns_zero a
     end.
 
@@ -495,7 +495,7 @@ Section TypedSyntaxFunctions.
     | @Unop _ _ _ _ _ _ _ _ fn _ => Some (PrimSignatures.Sigma1 fn).(retSig)
     | @Binop _ _ _ _ _ _ _ _ fn _ _ => Some (PrimSignatures.Sigma2 fn).(retSig)
     | @ExternalCall _ _ _ _ _ _ _ _ _ _ => None
-    | @InternalCall _ _ _ _ _ _ _ _ tau _ _ _ _ => Some tau
+    | @InternalCall _ _ _ _ _ _ _ _ tau _ _ _ => Some tau
     | @APos _ _ _ _ _ _ _ _ tau _ _ => Some tau
     end.
 
@@ -521,7 +521,7 @@ Section TypedSyntaxFunctions.
       let/opt r2 := interp_arithmetic arg2 in
       Some (PrimSpecs.sigma2 fn r1 r2)
     | ExternalCall fn arg => None
-    | InternalCall fn args body => None
+    | InternalCall fn args => None
     | APos pos a => interp_arithmetic a
     end.
 
@@ -544,8 +544,8 @@ Section TypedSyntaxFunctions.
            action_size arg1 + action_size arg2
          | ExternalCall ufn arg =>
            action_size arg
-         | InternalCall fn argspec body =>
-           cfoldl (fun _ arg acc => acc + action_size arg) argspec (action_size body)
+         | InternalCall fn argspec =>
+           cfoldl (fun _ arg acc => acc + action_size arg) argspec (action_size fn.(int_body))
          | APos p e => action_size e
          | _ => 0
          end)%N.
@@ -585,9 +585,9 @@ Section TypedSyntaxFunctions.
         find_read1s_after_write1s' acc arg2
       | ExternalCall fn arg =>
         find_read1s_after_write1s' acc arg
-      | InternalCall fn args body =>
+      | InternalCall fn args =>
         let acc := cfoldr (fun _ _ arg acc => find_read1s_after_write1s' acc arg) args acc in
-        find_read1s_after_write1s' acc body
+        find_read1s_after_write1s' acc fn.(int_body)
       | APos _ a => find_read1s_after_write1s' acc a
       end.
 
diff --git a/coq/TypedSyntaxProperties.v b/coq/TypedSyntaxProperties.v
index 5905e4b3..c907be8d 100644
--- a/coq/TypedSyntaxProperties.v
+++ b/coq/TypedSyntaxProperties.v
@@ -45,15 +45,14 @@ Section TypedSyntaxProperties.
     | [ H: Some _ = Some _ |- _ ] => inversion H; subst; clear H
     | _ => solve [intuition eauto 3 using bits_to_N_zero]
     end.
-
-  Lemma returns_zero_correct {sig tau} :
-    forall (a: action sig tau) (Gamma: tcontext sig) (sched_log: Log) (action_log: Log),
+  Fixpoint returns_zero_correct {sig tau} (a: action sig tau) {struct a} :
+    forall (Gamma: tcontext sig) (sched_log: Log) (action_log: Log),
       returns_zero a = true ->
       forall l v G,
         interp_action r sigma Gamma sched_log action_log a = Some (l, v, G) ->
         bits_of_value v = Bits.zeroes (type_sz tau).
   Proof.
-    induction a; repeat dec_step.
+    destruct a; try solve [repeat dec_step].
   Qed.
 
   Lemma is_pure_correct :
@@ -70,11 +69,12 @@ Section TypedSyntaxProperties.
                interp_args r sigma Gamma sched_log action_log args = Some (l', v, G) ->
                l = action_log).
 
-    { clear dependent a; clear t t2 Heqo.
+    { destruct fn as [name a]; clear dependent a.
+      clear t t2 Heqo.
       generalize dependent Gamma.
       generalize dependent sched_log.
       generalize dependent action_log.
-      generalize dependent (rev argspec); clear argspec.
+      generalize dependent (argspec).
       fix IHargs 2; destruct args; cbn; intros;
         repeat dec_step. }
 
diff --git a/coq/Types.v b/coq/Types.v
index 2a56238b..092a5c2e 100644
--- a/coq/Types.v
+++ b/coq/Types.v
@@ -289,21 +289,28 @@ Definition CExternalSignature := CSig 1.
 Definition tsig var_t := list (var_t * type).
 Definition lsig := list nat.
 
-Record InternalFunction {var_t fn_name_t action: Type} :=
+Record UInternalFunction' {var_t fn_name_t action: Type} :=
+  { uint_name : fn_name_t;
+    uint_argspec : tsig var_t;
+    uint_retType : type;
+    uint_body : action }.
+Arguments UInternalFunction' : clear implicits.
+Arguments Build_UInternalFunction' {var_t fn_name_t action}
+          uint_name uint_argspec uint_retType uint_body : assert.
+
+Definition map_uintf_body {var_t fn_name_t action action': Type}
+           (f: action -> action') (fn: UInternalFunction' var_t fn_name_t action) :=
+  {| uint_name := fn.(uint_name);
+     uint_argspec := fn.(uint_argspec);
+     uint_retType := fn.(uint_retType);
+     uint_body := f fn.(uint_body) |}.
+
+Record InternalFunction' {fn_name_t action: Type} :=
   { int_name : fn_name_t;
-    int_argspec : tsig var_t;
-    int_retSig : type;
     int_body : action }.
-Arguments InternalFunction : clear implicits.
-Arguments Build_InternalFunction {var_t fn_name_t action}
-          int_name int_argspec int_retSig int_body : assert.
-
-Definition map_intf_body {var_t fn_name_t action action': Type}
-           (f: action -> action') (fn: InternalFunction var_t fn_name_t action) :=
-  {| int_name := fn.(int_name);
-     int_argspec := fn.(int_argspec);
-     int_retSig := fn.(int_retSig);
-     int_body := f fn.(int_body) |}.
+Arguments InternalFunction' : clear implicits.
+Arguments Build_InternalFunction' {fn_name_t action}
+          int_name int_body : assert.
 
 Record arg_sig {var_t} :=
   { arg_name: var_t;
diff --git a/ocaml/backends/coq.ml b/ocaml/backends/coq.ml
index ca167028..686033d3 100644
--- a/ocaml/backends/coq.ml
+++ b/ocaml/backends/coq.ml
@@ -143,11 +143,11 @@ let pp_external_sig ppf f =
 let pp_internal_sig_arg ppf (nm, tau) =
   fprintf ppf "@[%a@ :: %a@]" pp_quoted nm (pp_type ~wrap:false) tau
 
-let pp_internal_function ppf (f: _ internal_function) =
+let pp_uinternal_function ppf (f: _ uinternal_function) =
   fprintf ppf "{{{ %a | %a ~> %a }}}"
-    pp_quoted f.int_name
-    (pp_seq (pp_sep " ~> ") pp_internal_sig_arg) f.int_argspec
-    (pp_type ~wrap:false) f.int_retSig
+    pp_quoted f.uint_name
+    (pp_seq (pp_sep " ~> ") pp_internal_sig_arg) f.uint_argspec
+    (pp_type ~wrap:false) f.uint_retType
 
 let pp_ext_fn_Sigma ppf (extfuns: ffi_signature list) =
   fprintf ppf "@[<hv 2>Definition Sigma (f: ext_fn_t): ExternalSignature :=@ %a@]."
@@ -318,7 +318,7 @@ let rec pp_action print_positions ppf (a: ResolvedAST.uaction locd) =
     | ExternalCall { fn; arg } ->
        pp_app "UExternalCall" "%a@ %a" pp_raw fn.lcnt.ffi_name pp_action arg
     | InternalCall { fn; args } ->
-       pp_app "UInternalCall" "%a@ %a" pp_raw fn.int_name (pp_list pp_action) args
+       pp_app "UInternalCall" "%a@ %a" pp_raw fn.uint_name (pp_list pp_action) args
     | Sugar u -> pp_app "USugar" "%a" pp_sugar u
   and pp_sugar ppf u =
     let pp_app fn fmt = pp_app ppf fn fmt in
@@ -367,13 +367,13 @@ let pp_scheduler print_positions ppf (name, scheduler) =
   fprintf ppf "@[<2>Definition %s_eval (sigma: forall f, Sigma f)@ : Log R ContextEnv :=@ " name;
   fprintf ppf "@[<2>interp_scheduler@ (ContextEnv.(create) r)@ sigma@ rules@ %s@].@]" name
 
-let pp_int_fn ~print_positions ppf (_, { int_name; int_argspec; int_retSig; int_body }) =
+let pp_int_fn ~print_positions ppf (_, { uint_name; uint_argspec; uint_retType; uint_body }) =
   let p fmt = fprintf ppf fmt in
-  p "@[<v>@[<hv 2>Definition %s {reg_t ext_fn_t} : UInternalFunction reg_t ext_fn_t := {|@ " int_name;
-  p "int_name := %a;@ " pp_quoted int_name;
-  p "int_argspec := %a;@ " (pp_list (pp_pair pp_quoted pp_type_unwrapped)) int_argspec;
-  p "int_retSig := %a;@ " pp_type_unwrapped int_retSig;
-  p "int_body := %a;" (pp_action print_positions) int_body;
+  p "@[<v>@[<hv 2>Definition %s {reg_t ext_fn_t} : UInternalFunction reg_t ext_fn_t := {|@ " uint_name;
+  p "uint_name := %a;@ " pp_quoted uint_name;
+  p "uint_argspec := %a;@ " (pp_list (pp_pair pp_quoted pp_type_unwrapped)) uint_argspec;
+  p "uint_retType := %a;@ " pp_type_unwrapped uint_retType;
+  p "uint_body := %a;" (pp_action print_positions) uint_body;
   p "@]@ |}.@]"
 
 let pp_tc_rules ppf (rules: (string * _) list) =
diff --git a/ocaml/backends/cpp.ml b/ocaml/backends/cpp.ml
index 3100ca61..66330c44 100644
--- a/ocaml/backends/cpp.ml
+++ b/ocaml/backends/cpp.ml
@@ -1114,11 +1114,11 @@ them before writing to the registers.\n"
         let bindings, body = loop pos [] action in
         List.rev bindings, body in
 
-      let package_intfun fn argspec tau body =
-        { Extr.int_name = hpp.cpp_fn_names fn;
-          Extr.int_argspec = argspec;
-          Extr.int_retSig = tau;
-          Extr.int_body = body } in
+      let package_intfun fn argspec tau =
+        { Extr.uint_name = hpp.cpp_fn_names fn.Extr.int_name;
+          Extr.uint_argspec = argspec;
+          Extr.uint_retType = tau;
+          Extr.uint_body = fn.Extr.int_body } in
 
       (* Table mapping function objects to unique names.  This is reset for each
          rules, because each implementation of a function is specific to one
@@ -1126,8 +1126,8 @@ them before writing to the registers.\n"
          to invoke a rule-specific reset function *)
       let internal_functions = Hashtbl.create 20 in
 
-      let lookup_intfun fn argspec tau body =
-        let intf = package_intfun fn argspec tau body in
+      let lookup_intfun fn argspec tau =
+        let intf = package_intfun fn argspec tau in
         intf, Hashtbl.find_opt internal_functions intf in
 
       let rec p_action
@@ -1229,8 +1229,8 @@ them before writing to the registers.\n"
            (* See ‘Read’ case for why returning just ImpureExpr isn't safe *)
            let expr = cpp_ext_funcall ffi.ffi_name kind (must_value a) in
            p_assign_impure target (ImpureExpr expr)
-        | Extr.InternalCall (_, tau, fn, argspec, rev_args, body) ->
-           let fn_name = match snd (lookup_intfun fn argspec tau body) with
+        | Extr.InternalCall (_, tau, argspec, fn, rev_args) ->
+           let fn_name = match snd (lookup_intfun fn argspec tau) with
              | Some fn -> fn
              | None -> assert false in
            let args = Extr.cfoldl (fun (argname, tau) arg argstrs ->
@@ -1314,15 +1314,15 @@ them before writing to the registers.\n"
             else
               loop (counter + 1) in
           loop 0 in
-        let register_intfun pos fn argspec tau body =
+        let register_intfun pos fn argspec tau =
           assert_no_duplicates ~descr:"argument list"
             (List.map (fun (v, _) -> hpp.cpp_var_names v) argspec);
-          match lookup_intfun fn argspec tau body with
+          match lookup_intfun fn argspec tau with
           | _, Some _ -> ()
           | intf, None ->
-             let nm = ensure_fresh (hpp.cpp_fn_names fn) in
+             let nm = ensure_fresh (hpp.cpp_fn_names fn.Extr.int_name) in
              fns := (pos, nm, intf) :: !fns;
-             Hashtbl.add internal_functions intf nm in
+             Hashtbl.add internal_functions intf nm; in
         let rec loop pos = function
           | Extr.Fail _
             | Extr.Var _
@@ -1343,10 +1343,10 @@ them before writing to the registers.\n"
              loop pos c;
              loop pos tbr;
              loop pos fbr
-          | Extr.InternalCall (_, tau, fn, argspec, rev_args, body) ->
-             register_intfun pos fn argspec tau body;
+          | Extr.InternalCall (_, tau, argspec, fn, rev_args) ->
+             register_intfun pos fn argspec tau;
              Extr.cfoldr (fun _ _ arg () -> loop pos arg) argspec rev_args ();
-             loop pos body in
+             loop pos fn.Extr.int_body in
         loop pos action;
         List.rev !fns in
 
@@ -1354,14 +1354,14 @@ them before writing to the registers.\n"
         let sp_arg (nm, tau) =
           let tau = Cuttlebone.Util.typ_of_extr_type tau in
           sprintf "%s %s" (cpp_type_of_type tau) (hpp.cpp_var_names nm) in
-        let ret_tau = Cuttlebone.Util.typ_of_extr_type intf.Extr.int_retSig in
+        let ret_tau = Cuttlebone.Util.typ_of_extr_type intf.Extr.uint_retType in
         let ret_type = cpp_type_of_type ret_tau in
         let ret_arg = sprintf "%s %s" ret_type "&_ret" in
-        let args = String.concat ", " @@ name :: ret_arg :: List.map sp_arg intf.Extr.int_argspec in
+        let args = String.concat ", " @@ name :: ret_arg :: List.map sp_arg intf.Extr.uint_argspec in
         p "DECL_FN(%s, %s)" name ret_type;
         p_special_fn "FN" ~args (fun () ->
             let target = VarTarget { tau = ret_tau; declared = true; name = "_ret" } in
-            p_assign_and_ignore target (p_action true pos target intf.int_body);
+            p_assign_and_ignore target (p_action true pos target intf.uint_body);
             p "return true;") in
 
       p "#define RULE_NAME %s" rule_name_unprefixed;
diff --git a/ocaml/common/common.ml b/ocaml/common/common.ml
index f15ec920..262431e9 100644
--- a/ocaml/common/common.ml
+++ b/ocaml/common/common.ml
@@ -250,11 +250,11 @@ let locd_make lpos lcnt =
 let locd_of_pair (pos, x) =
   locd_make pos x
 
-type 'action internal_function = {
-    int_name: string;
-    int_argspec: (string * typ) list;
-    int_retSig: typ;
-    int_body: 'action
+type 'action uinternal_function = {
+    uint_name: string;
+    uint_argspec: (string * typ) list;
+    uint_retType: typ;
+    uint_body: 'action
   }
 
 let with_output_to_file fname (f: out_channel -> 'a -> unit) (data: 'a) =
diff --git a/ocaml/cuttlebone/cuttlebone.ml b/ocaml/cuttlebone/cuttlebone.ml
index ce3fb940..e733bb2f 100644
--- a/ocaml/cuttlebone/cuttlebone.ml
+++ b/ocaml/cuttlebone/cuttlebone.ml
@@ -92,17 +92,17 @@ module Util = struct
     Extr.{ argSigs = Extr.vect_of_list [extr_type_of_typ ffi_argtype];
           retSig = extr_type_of_typ ffi_rettype }
 
-  let extr_intfun_of_intfun fbody (fsig: _ Common.internal_function) =
-    { Extr.int_name = fsig.int_name;
-      Extr.int_argspec = List.map (fun (nm, tau) -> nm, extr_type_of_typ tau) fsig.int_argspec;
-      Extr.int_retSig = extr_type_of_typ fsig.int_retSig;
-      Extr.int_body = fbody fsig.int_body }
-
-  let intfun_of_extr_intfun fbody (fsig: _ Extr.internalFunction) =
-    { int_name = fsig.int_name;
-      int_argspec = List.map (fun (nm, tau) -> nm, typ_of_extr_type tau) fsig.int_argspec;
-      int_retSig = typ_of_extr_type fsig.int_retSig;
-      int_body = fbody fsig.int_body }
+  let extr_uintfun_of_uintfun fbody (fsig: _ Common.uinternal_function) =
+    { Extr.uint_name = fsig.uint_name;
+      Extr.uint_argspec = List.map (fun (nm, tau) -> nm, extr_type_of_typ tau) fsig.uint_argspec;
+      Extr.uint_retType = extr_type_of_typ fsig.uint_retType;
+      Extr.uint_body = fbody fsig.uint_body }
+
+  let uintfun_of_extr_uintfun fbody (fsig: _ Extr.uInternalFunction') =
+    { uint_name = fsig.uint_name;
+      uint_argspec = List.map (fun (nm, tau) -> nm, typ_of_extr_type tau) fsig.uint_argspec;
+      uint_retType = typ_of_extr_type fsig.uint_retType;
+      uint_body = fbody fsig.uint_body }
 
   let extr_type_to_string tau =
     typ_to_string (typ_of_extr_type tau)
diff --git a/ocaml/frontends/lv.ml b/ocaml/frontends/lv.ml
index cad77351..59a33394 100644
--- a/ocaml/frontends/lv.ml
+++ b/ocaml/frontends/lv.ml
@@ -83,7 +83,7 @@ module ResolvedAST = struct
     | Unop of { fn: (Extr.PrimUntyped.ufn1) locd; arg: uaction locd }
     | Binop of { fn: (Extr.PrimUntyped.ufn2) locd; a1: uaction locd; a2: uaction locd }
     | ExternalCall of { fn: ffi_signature locd; arg: uaction locd }
-    | InternalCall of { fn: uaction locd internal_function; args: uaction locd list }
+    | InternalCall of { fn: uaction locd uinternal_function; args: uaction locd list }
     | Sugar of usugar
   and usugar =
     | AstError
@@ -116,7 +116,7 @@ module ResolvedAST = struct
        | ExternalCall { fn; arg } -> UExternalCall (fn.lcnt, translate_action arg)
        | InternalCall { fn; args } ->
           UInternalCall
-            (Util.extr_intfun_of_intfun translate_action fn,
+            (Util.extr_uintfun_of_uintfun translate_action fn,
              List.map translate_action args)
        | Sugar u ->
           Extr.USugar
@@ -198,7 +198,7 @@ type unresolved_unit = {
 type resolved_extfun = ffi_signature
 
 type resolved_defun =
-  ResolvedAST.uaction locd internal_function
+  ResolvedAST.uaction locd uinternal_function
 
 type resolved_fn =
   | FnExternal of ffi_signature
@@ -1605,10 +1605,10 @@ let resolve_fn_decl types fns { ufn_name; ufn_signature; ufn_rettype; ufn_body }
    match ufn_body with
    | InternalUfn body ->
       let body = resolve_action types fns [] body in
-      InternalDecl { int_name = ufn_name.lcnt;
-                     int_retSig = rettype;
-                     int_argspec = args;
-                     int_body = body }
+      InternalDecl { uint_name = ufn_name.lcnt;
+                     uint_retType = rettype;
+                     uint_argspec = args;
+                     uint_body = body }
    | ExternalUfn ->
       let unit_t = Bits_t 0 in
       let ffi_argtype = match List.map snd args with