# HG changeset patch # User wenzelm # Date 1563704882 -7200 # Node ID 35dd9212bf295c468667dc64040d8d43a96b8944 # Parent 6af87375b95f827247ca5e56729bb53e999692f7 tuned; diff -r 6af87375b95f -r 35dd9212bf29 src/HOL/Tools/SMT/smt_builtin.ML --- 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>\type\) + val aT = Term.aT \<^sort>\type\ val c = (\<^const_name>\HOL.eq\, aT --> aT --> \<^typ>\bool\) fun mk ts = Term.list_comb (HOLogic.eq_const (Term.fastype_of (hd ts)), ts) in diff -r 6af87375b95f -r 35dd9212bf29 src/Pure/Isar/class.ML --- 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; diff -r 6af87375b95f -r 35dd9212bf29 src/Pure/Isar/class_declaration.ML --- 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 diff -r 6af87375b95f -r 35dd9212bf29 src/Pure/Isar/object_logic.ML --- 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)); diff -r 6af87375b95f -r 35dd9212bf29 src/Pure/Proof/proof_syntax.ML --- 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 **) diff -r 6af87375b95f -r 35dd9212bf29 src/Pure/axclass.ML --- 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); diff -r 6af87375b95f -r 35dd9212bf29 src/Tools/Code/code_runtime.ML --- 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