author wenzelm Mon, 04 Oct 2021 19:17:50 +0200 changeset 74448 2fd74a2c4e1c parent 74447 5f9c51c2fc0a child 74449 a2dcda6107d9
clarified signature;
 src/CCL/Term.thy file | annotate | diff | comparison | revisions src/Pure/Syntax/syntax_trans.ML file | annotate | diff | comparison | revisions
```--- a/src/CCL/Term.thy	Mon Oct 04 19:12:24 2021 +0200
+++ b/src/CCL/Term.thy	Mon Oct 04 19:17:50 2021 +0200
@@ -88,30 +88,30 @@

fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
let
-        val (f',b') = Syntax_Trans.variant_abs'(ff,SS,b)
-        val (_,a'') = Syntax_Trans.variant_abs'(f,S,a)
-        val (x',a') = Syntax_Trans.variant_abs'(x,T,a'')
+        val (f',b') = Syntax_Trans.print_abs(ff,SS,b)
+        val (_,a'') = Syntax_Trans.print_abs(f,S,a)
+        val (x',a') = Syntax_Trans.print_abs(x,T,a'')
in
Syntax.const \<^syntax_const>\<open>_letrec\<close> \$ bound(f',SS) \$ bound(x',T) \$ a' \$ b'
end;

fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
let
-        val (f',b') = Syntax_Trans.variant_abs'(ff,SS,b)
-        val ( _,a1) = Syntax_Trans.variant_abs'(f,S,a)
-        val (y',a2) = Syntax_Trans.variant_abs'(y,U,a1)
-        val (x',a') = Syntax_Trans.variant_abs'(x,T,a2)
+        val (f',b') = Syntax_Trans.print_abs(ff,SS,b)
+        val ( _,a1) = Syntax_Trans.print_abs(f,S,a)
+        val (y',a2) = Syntax_Trans.print_abs(y,U,a1)
+        val (x',a') = Syntax_Trans.print_abs(x,T,a2)
in
Syntax.const \<^syntax_const>\<open>_letrec2\<close> \$ bound(f',SS) \$ bound(x',T) \$ bound(y',U) \$ a' \$ b'
end;

fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
let
-        val (f',b') = Syntax_Trans.variant_abs'(ff,SS,b)
-        val ( _,a1) = Syntax_Trans.variant_abs'(f,S,a)
-        val (z',a2) = Syntax_Trans.variant_abs'(z,V,a1)
-        val (y',a3) = Syntax_Trans.variant_abs'(y,U,a2)
-        val (x',a') = Syntax_Trans.variant_abs'(x,T,a3)
+        val (f',b') = Syntax_Trans.print_abs(ff,SS,b)
+        val ( _,a1) = Syntax_Trans.print_abs(f,S,a)
+        val (z',a2) = Syntax_Trans.print_abs(z,V,a1)
+        val (y',a3) = Syntax_Trans.print_abs(y,U,a2)
+        val (x',a') = Syntax_Trans.print_abs(x,T,a3)
in
Syntax.const \<^syntax_const>\<open>_letrec3\<close> \$
bound(f',SS) \$ bound(x',T) \$ bound(y',U) \$ bound(z',V) \$ a' \$ b'```
```--- a/src/Pure/Syntax/syntax_trans.ML	Mon Oct 04 19:12:24 2021 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Mon Oct 04 19:17:50 2021 +0200
@@ -38,8 +38,7 @@
val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term)
val preserve_binder_abs_tr': string -> string -> string * (Proof.context -> term list -> term)
val preserve_binder_abs2_tr': string -> string -> string * (Proof.context -> term list -> term)
-  val variant_abs: string * typ * term -> string * term
-  val variant_abs': string * typ * term -> string * term
+  val print_abs: string * typ * term -> string * term
val dependent_tr': string * string -> term list -> term
val antiquote_tr': string -> term -> term
val quote_tr': string -> term -> term
@@ -389,16 +388,13 @@

(* dependent / nondependent quantifiers *)

-fun var_abs mark (x, T, b) =
+fun print_abs (x, T, b) =
let val (x', _) = Name.variant x (Term.declare_term_names b Name.context)
-  in (x', subst_bound (mark (x', T), b)) end;
-
-val variant_abs = var_abs Free;
-val variant_abs' = var_abs mark_bound_abs;
+  in (x', subst_bound (mark_bound_abs (x', T), b)) end;

fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
if Term.is_dependent B then
-        let val (x', B') = variant_abs' (x, dummyT, B);
+        let val (x', B') = print_abs (x, dummyT, B);
in Term.list_comb (Syntax.const q \$ mark_bound_abs (x', T) \$ A \$ B', ts) end
else Term.list_comb (Syntax.const r \$ A \$ incr_boundvars ~1 B, ts)
| dependent_tr' _ _ = raise Match;```