--- a/src/HOL/Tools/SMT/smt_builtin.ML Sun Jul 21 12:11:35 2019 +0200
+++ b/src/HOL/Tools/SMT/smt_builtin.ML Sun Jul 21 12:28:02 2019 +0200
@@ -180,7 +180,7 @@
fun dest_builtin_eq ctxt t u =
let
- val aT = TFree (Name.aT, \<^sort>\<open>type\<close>)
+ val aT = Term.aT \<^sort>\<open>type\<close>
val c = (\<^const_name>\<open>HOL.eq\<close>, aT --> aT --> \<^typ>\<open>bool\<close>)
fun mk ts = Term.list_comb (HOLogic.eq_const (Term.fastype_of (hd ts)), ts)
in
--- a/src/Pure/Isar/class.ML Sun Jul 21 12:11:35 2019 +0200
+++ b/src/Pure/Isar/class.ML Sun Jul 21 12:28:02 2019 +0200
@@ -309,7 +309,7 @@
(case Vartab.lookup tyenv (Name.aT, 0) of
SOME (_, ty' as TVar (vi, sort)) =>
if Type_Infer.is_param vi andalso Sorts.sort_le algebra (base_sort, sort)
- then SOME (ty', TFree (Name.aT, base_sort))
+ then SOME (ty', Term.aT base_sort)
else NONE
| _ => NONE)
| NONE => NONE)
@@ -335,8 +335,7 @@
fun begin sort base_sort ctxt =
ctxt
- |> Variable.declare_term
- (Logic.mk_type (TFree (Name.aT, base_sort)))
+ |> Variable.declare_term (Logic.mk_type (Term.aT base_sort))
|> synchronize_class_syntax sort base_sort
|> Overloading.activate_improvable_syntax;
--- a/src/Pure/Isar/class_declaration.ML Sun Jul 21 12:11:35 2019 +0200
+++ b/src/Pure/Isar/class_declaration.ML Sun Jul 21 12:28:02 2019 +0200
@@ -41,7 +41,7 @@
val const_morph =
Element.instantiate_normalize_morphism ([], param_map_inst);
val typ_morph =
- Element.instantiate_normalize_morphism ([(a_tfree, certT (TFree (Name.aT, [class])))], [])
+ Element.instantiate_normalize_morphism ([(a_tfree, certT (Term.aT [class]))], [])
val (([raw_props], _, [(_, raw_inst_morph)], _, export_morph), _) = thy_ctxt
|> Expression.cert_goal_expression ([(class, (("", false),
(Expression.Named param_map_const, [])))], []);
@@ -139,7 +139,7 @@
" of type parameter " ^ Name.aT ^ " of sort " ^
Syntax.string_of_sort_global thy S)
| _ => error "Multiple type variables in class specification");
- val fixateT = TFree (Name.aT, fixate_sort);
+ val fixateT = Term.aT fixate_sort;
in
(map o map_atyps)
(fn T as TVar (xi, _) => if Type_Infer.is_param xi then fixateT else T | T => T) Ts
@@ -194,7 +194,7 @@
| [(_, sort)] => sort
| _ => error "Multiple type variables in class specification");
val supparams = map (fn ((c, T), _) =>
- (c, map_atyps (K (TFree (Name.aT, base_sort))) T)) raw_supparams;
+ (c, map_atyps (K (Term.aT base_sort)) T)) raw_supparams;
val supparam_names = map fst supparams;
fun mk_param ((c, _), _) = Free (c, (the o AList.lookup (op =) supparams) c);
val supexpr = (map (fn sup => (sup, (("", false),
@@ -264,16 +264,16 @@
(*FIXME simplify*)
val supconsts = supparam_names
|> AList.make (snd o the o AList.lookup (op =) (Class.these_params thy sups))
- |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
+ |> (map o apsnd o apsnd o map_atyps) (K (Term.aT [class]));
val all_params = Locale.params_of thy class;
val raw_params = (snd o chop (length supparam_names)) all_params;
fun add_const ((raw_c, raw_ty), _) thy =
let
val b = Binding.name raw_c;
val c = Sign.full_name thy b;
- val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
+ val ty = map_atyps (K (Term.aT base_sort)) raw_ty;
val ty0 = Type.strip_sorts ty;
- val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0;
+ val ty' = map_atyps (K (Term.aT [class])) ty0;
val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b;
in
thy
--- a/src/Pure/Isar/object_logic.ML Sun Jul 21 12:11:35 2019 +0200
+++ b/src/Pure/Isar/object_logic.ML Sun Jul 21 12:28:02 2019 +0200
@@ -126,7 +126,7 @@
fun fixed_judgment ctxt x =
let (*be robust wrt. low-level errors*)
val c = judgment_name ctxt;
- val aT = TFree (Name.aT, []);
+ val aT = Term.aT [];
val T =
the_default (aT --> propT) (Sign.const_type (Proof_Context.theory_of ctxt) c)
|> Term.map_type_tvar (fn ((a, _), S) => TFree (a, S));
--- a/src/Pure/Proof/proof_syntax.ML Sun Jul 21 12:11:35 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Sun Jul 21 12:28:02 2019 +0200
@@ -28,7 +28,7 @@
val paramT = Type ("param", []);
val paramsT = Type ("params", []);
val idtT = Type ("idt", []);
-val aT = TFree (Name.aT, []);
+val aT = Term.aT [];
(** constants for theorems and axioms **)
--- a/src/Pure/axclass.ML Sun Jul 21 12:11:35 2019 +0200
+++ b/src/Pure/axclass.ML Sun Jul 21 12:28:02 2019 +0200
@@ -512,7 +512,7 @@
(case Term.add_tvarsT T [] of
[((a, _), S)] => check_constraint (a, S)
| _ => error ("Exactly one type variable expected in class parameter " ^ quote p));
- val T' = Term.map_type_tvar (fn _ => TFree (Name.aT, [class])) T;
+ val T' = Term.map_type_tvar (K (Term.aT [class])) T;
in (p, T') end);
--- a/src/Tools/Code/code_runtime.ML Sun Jul 21 12:11:35 2019 +0200
+++ b/src/Tools/Code/code_runtime.ML Sun Jul 21 12:28:02 2019 +0200
@@ -542,8 +542,9 @@
val position_index' = #position_index data + 1;
fun generated_code' () =
let
- val evals = Abs ("eval", map snd computation_cTs' --->
- TFree (Name.aT, []), list_comb (Bound 0, map Const computation_cTs'))
+ val evals =
+ Abs ("eval", map snd computation_cTs' ---> Term.aT [],
+ list_comb (Bound 0, map Const computation_cTs'))
|> preprocess_term { ctxt = ctxt } ctxt
in Code_Thingol.dynamic_value ctxt
(K I) (runtime_code ctxt NONE [] named_consts' computation_Ts') evals