src/Pure/Isar/class.ML
changeset 24748 ee0a0eb6b738
parent 24731 c25aa6ae64ec
child 24766 d0de4e48b526
     1.1 --- a/src/Pure/Isar/class.ML	Fri Sep 28 10:35:53 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Sat Sep 29 08:58:51 2007 +0200
     1.3 @@ -13,9 +13,9 @@
     1.4      -> ((bstring * Attrib.src list) * string list) list
     1.5      -> theory -> class * theory
     1.6    val classrel_cmd: xstring * xstring -> theory -> Proof.state
     1.7 -  val class: bstring -> class list -> Element.context_i Locale.element list
     1.8 +  val class: bool -> bstring -> class list -> Element.context_i Locale.element list
     1.9      -> string list -> theory -> string * Proof.context
    1.10 -  val class_cmd: bstring -> xstring list -> Element.context Locale.element list
    1.11 +  val class_cmd: bool -> bstring -> xstring list -> Element.context Locale.element list
    1.12      -> xstring list -> theory -> string * Proof.context
    1.13    val add_const_in_class: string -> (string * term) * Syntax.mixfix
    1.14      -> theory -> theory
    1.15 @@ -25,6 +25,7 @@
    1.16    val intro_classes_tac: thm list -> tactic
    1.17    val default_intro_classes_tac: thm list -> tactic
    1.18    val class_of_locale: theory -> string -> class option
    1.19 +  val local_syntax: theory -> class -> bool
    1.20    val print_classes: theory -> unit
    1.21  
    1.22    val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
    1.23 @@ -46,12 +47,12 @@
    1.24    val params_of_sort: theory -> sort -> (string * (string * typ)) list
    1.25  
    1.26    (*experimental*)
    1.27 -  val init_ref: (class -> Proof.context -> (theory -> theory) * Proof.context) ref
    1.28 -  val init: class -> Proof.context -> (theory -> theory) * Proof.context;
    1.29 -  val init_default: class -> Proof.context -> (theory -> theory) * Proof.context;
    1.30 -  val remove_constraints: class -> theory -> (string * typ) list * theory
    1.31 -  val class_term_check: theory -> class -> term list -> Proof.context -> term list * Proof.context
    1.32 -  val local_param: theory -> class -> string -> (term * (class * int)) option
    1.33 +  val init_ref: (sort -> Proof.context -> Proof.context) ref
    1.34 +  val init: sort -> Proof.context -> Proof.context;
    1.35 +  val init_default: sort -> Proof.context -> Proof.context;
    1.36 +  val local_param: theory -> sort -> string -> (term * (class * int)) option
    1.37 +  val remove_constraints': sort -> theory -> (string * typ) list * theory
    1.38 +  val remove_constraints: sort -> Proof.context -> (string * typ) list * Proof.context
    1.39  end;
    1.40  
    1.41  structure Class : CLASS =
    1.42 @@ -99,7 +100,7 @@
    1.43        | NONE => thm;
    1.44    in strip end;
    1.45  
    1.46 -fun get_remove_contraint c thy =
    1.47 +fun get_remove_constraint c thy =
    1.48    let
    1.49      val ty = Sign.the_const_constraint thy c;
    1.50    in
    1.51 @@ -298,7 +299,7 @@
    1.52        #> after_qed defs;
    1.53    in
    1.54      theory
    1.55 -    |> fold_map get_remove_contraint (map fst cs |> distinct (op =))
    1.56 +    |> fold_map get_remove_constraint (map fst cs |> distinct (op =))
    1.57      ||>> fold_map add_def defs
    1.58      ||> fold (fn (c, ((class, tyco), ty)) => add_inst_def' (class, tyco) (c, ty)) other_cs
    1.59      |-> (fn (cs, defs) => do_proof (after_qed' cs defs) arities defs)
    1.60 @@ -329,26 +330,27 @@
    1.61    locale: string,
    1.62    consts: (string * string) list
    1.63      (*locale parameter ~> theory constant name*),
    1.64 -  v: string,
    1.65 +  local_sort: sort,
    1.66    inst: typ Symtab.table * term Symtab.table
    1.67      (*canonical interpretation*),
    1.68    intro: thm,
    1.69 +  local_syntax: bool,
    1.70    defs: thm list,
    1.71    localized: (string * (term * (class * int))) list
    1.72      (*theory constant name ~> (locale parameter, (class, instantiaton index of class typ))*)
    1.73  };
    1.74  
    1.75  fun rep_class_data (ClassData d) = d;
    1.76 -fun mk_class_data ((locale, consts, v, inst, intro), (defs, localized)) =
    1.77 -  ClassData { locale = locale, consts = consts, v = v, inst = inst, intro = intro,
    1.78 -    defs = defs, localized = localized };
    1.79 -fun map_class_data f (ClassData { locale, consts, v, inst, intro, defs, localized }) =
    1.80 -  mk_class_data (f ((locale, consts, v, inst, intro), (defs, localized)))
    1.81 -fun merge_class_data _ (ClassData { locale = locale, consts = consts, v = v, inst = inst,
    1.82 -    intro = intro, defs = defs1, localized = localized1 },
    1.83 -  ClassData { locale = _, consts = _, v = _, inst = _, intro = _,
    1.84 +fun mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax), (defs, localized)) =
    1.85 +  ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst, intro = intro,
    1.86 +    local_syntax = local_syntax, defs = defs, localized = localized };
    1.87 +fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro, local_syntax, defs, localized }) =
    1.88 +  mk_class_data (f ((locale, consts, local_sort, inst, intro, local_syntax), (defs, localized)))
    1.89 +fun merge_class_data _ (ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst,
    1.90 +    intro = intro, local_syntax = local_syntax, defs = defs1, localized = localized1 },
    1.91 +  ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _, local_syntax = _,
    1.92      defs = defs2, localized = localized2 }) =
    1.93 -  mk_class_data ((locale, consts, v, inst, intro),
    1.94 +  mk_class_data ((locale, consts, local_sort, inst, intro, local_syntax),
    1.95      (Thm.merge_thms (defs1, defs2), AList.merge (op =) (K true) (localized1, localized2)));
    1.96  
    1.97  fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));
    1.98 @@ -393,11 +395,13 @@
    1.99    Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_class_data) data))
   1.100      ((fst o ClassData.get) thy) [];
   1.101  
   1.102 -fun these_localized thy class =
   1.103 -  maps (#localized o the_class_data thy) (ancestry thy [class]);
   1.104 +fun these_localized thy =
   1.105 +  maps (#localized o the_class_data thy) o ancestry thy;
   1.106  
   1.107  fun local_param thy = AList.lookup (op =) o these_localized thy;
   1.108  
   1.109 +fun local_syntax thy = #local_syntax o the_class_data thy
   1.110 +
   1.111  fun print_classes thy =
   1.112    let
   1.113      val algebra = Sign.classes_of thy;
   1.114 @@ -433,11 +437,11 @@
   1.115  
   1.116  (* updaters *)
   1.117  
   1.118 -fun add_class_data ((class, superclasses), (locale, consts, v, inst, intro)) =
   1.119 +fun add_class_data ((class, superclasses), (locale, consts, local_sort, inst, intro, local_syntax)) =
   1.120    ClassData.map (fn (gr, tab) => (
   1.121      gr
   1.122 -    |> Graph.new_node (class, mk_class_data ((locale, (map o apfst) fst consts, v, inst, intro),
   1.123 -         ([], map (apsnd (rpair (class, 0) o Free) o swap) consts)))
   1.124 +    |> Graph.new_node (class, mk_class_data ((locale, (map o apfst) fst consts, local_sort, inst,
   1.125 +         intro, local_syntax), ([], map (apsnd (rpair (class, 0) o Free) o swap) consts)))
   1.126      |> fold (curry Graph.add_edge class) superclasses,
   1.127      tab
   1.128      |> Symtab.update (locale, class)
   1.129 @@ -539,6 +543,90 @@
   1.130  
   1.131  (** classes and class target **)
   1.132  
   1.133 +(* class context initialization *)
   1.134 +
   1.135 +(*experimental*)
   1.136 +fun get_remove_constraint_ctxt c ctxt =
   1.137 +  let
   1.138 +    val ty = ProofContext.the_const_constraint ctxt c;
   1.139 +  in
   1.140 +    ctxt
   1.141 +    |> ProofContext.add_const_constraint (c, NONE)
   1.142 +    |> pair (c, ty)
   1.143 +  end;
   1.144 +
   1.145 +fun remove_constraints' class thy =
   1.146 +  thy |> fold_map (get_remove_constraint o fst) (these_localized thy class);
   1.147 +
   1.148 +fun remove_constraints class ctxt =
   1.149 +  ctxt |> fold_map (get_remove_constraint_ctxt o fst) (these_localized (ProofContext.theory_of ctxt) class);
   1.150 +
   1.151 +fun default_typ ctxt constraints c =
   1.152 +  case AList.lookup (op =) constraints c
   1.153 +   of SOME ty => SOME ty
   1.154 +    | NONE => try (Consts.the_constraint (ProofContext.consts_of ctxt)) c;
   1.155 +
   1.156 +fun infer_constraints ctxt constraints ts =
   1.157 +    TypeInfer.infer_types (ProofContext.pp ctxt) (Sign.tsig_of (ProofContext.theory_of ctxt))
   1.158 +     (Syntax.check_typs ctxt)
   1.159 +      (default_typ ctxt constraints) (K NONE)
   1.160 +      (Variable.names_of ctxt) true (map (rpair dummyT) ts)
   1.161 +    |> #1 |> map #1
   1.162 +  handle TYPE (msg, _, _) => error msg
   1.163 +
   1.164 +fun subst_typ local_sort =
   1.165 +  map_atyps (fn (t as TFree (v, _)) => if v = AxClass.param_tyvarname
   1.166 +        then TFree (v, local_sort)
   1.167 +        else t
   1.168 +    | t => t);
   1.169 +
   1.170 +fun sort_typ_check thy sort =
   1.171 +  let
   1.172 +    val local_sort = (#local_sort o the_class_data thy) (hd sort);
   1.173 +  in
   1.174 +    pair o map (subst_typ local_sort)
   1.175 +  end;
   1.176 +
   1.177 +fun sort_term_check thy sort constraints =
   1.178 +  let
   1.179 +    val algebra = Sign.classes_of thy;
   1.180 +    val local_sort = (#local_sort o the_class_data thy) (hd sort);
   1.181 +    val v = AxClass.param_tyvarname;
   1.182 +    val local_param = local_param thy sort;
   1.183 +      (*FIXME efficiency*)
   1.184 +    fun class_arg c idx ty =
   1.185 +      let
   1.186 +        val typargs = Sign.const_typargs thy (c, ty);
   1.187 +        fun classtyp (TFree (w, _)) = w = v
   1.188 +          | classtyp t = false;
   1.189 +      in classtyp (nth typargs idx) end;
   1.190 +    fun subst (t as Const (c, ty)) = (case local_param c
   1.191 +         of NONE => t
   1.192 +          | SOME (t', (_, idx)) => if class_arg c idx ty
   1.193 +             then t' else t)
   1.194 +      | subst t = t;
   1.195 +  in fn ts => fn ctxt =>
   1.196 +    ((map (map_aterms subst) #> infer_constraints ctxt constraints) ts, ctxt)
   1.197 +  end;
   1.198 +
   1.199 +fun init_default sort ctxt =
   1.200 +  let
   1.201 +    val thy = ProofContext.theory_of ctxt;
   1.202 +    val typ_check = sort_typ_check thy sort;
   1.203 +    val term_check = sort_term_check thy sort;
   1.204 +  in
   1.205 +    ctxt
   1.206 +    |> remove_constraints sort
   1.207 +    ||> Variable.declare_term (Logic.mk_type (TFree (AxClass.param_tyvarname, sort)))
   1.208 +    ||> Context.proof_map (Syntax.add_typ_check typ_check)
   1.209 +    |-> (fn constraints =>
   1.210 +        Context.proof_map (Syntax.add_term_check (term_check constraints)))
   1.211 +  end;
   1.212 +
   1.213 +val init_ref = ref (K I : sort -> Proof.context -> Proof.context);
   1.214 +fun init class = ! init_ref class;
   1.215 +
   1.216 +
   1.217  (* class definition *)
   1.218  
   1.219  local
   1.220 @@ -551,52 +639,62 @@
   1.221      | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
   1.222    end;
   1.223  
   1.224 -fun gen_class add_locale prep_class prep_param bname
   1.225 -    raw_supclasses raw_elems raw_other_consts thy =
   1.226 +fun gen_class_spec prep_class prep_expr process_expr thy raw_supclasses raw_includes_elems =
   1.227    let
   1.228 +    val supclasses = map (prep_class thy) raw_supclasses;
   1.229 +    val sups = filter (is_some o lookup_class_data thy) supclasses
   1.230 +      |> Sign.minimize_sort thy;
   1.231 +    val supsort = Sign.minimize_sort thy supclasses;
   1.232 +    val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups;
   1.233 +    val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
   1.234 +      | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []);
   1.235 +    val supexpr = Locale.Merge suplocales;
   1.236 +    val supparams = (map fst o Locale.parameters_of_expr thy) supexpr;
   1.237 +    val supconsts = AList.make (the o AList.lookup (op =) (params_of_sort thy sups))
   1.238 +      (map fst supparams);
   1.239 +    val mergeexpr = Locale.Merge (suplocales @ includes);
   1.240 +    val constrain = Element.Constrains ((map o apsnd o map_atyps)
   1.241 +      (fn TFree (_, sort) => TFree (AxClass.param_tyvarname, sort)) supparams);
   1.242 +  in
   1.243 +    ProofContext.init thy
   1.244 +    |> Locale.cert_expr supexpr [constrain]
   1.245 +    |> snd
   1.246 +    |> init supsort
   1.247 +    |> process_expr Locale.empty raw_elems
   1.248 +    |> fst
   1.249 +    |> (fn elems => ((((sups, supconsts), (supsort, mergeexpr)),
   1.250 +          (*FIXME*) if null includes then constrain :: elems else elems)))
   1.251 +  end;
   1.252 +
   1.253 +val read_class_spec = gen_class_spec Sign.intern_class Locale.intern_expr Locale.read_expr;
   1.254 +val check_class_spec = gen_class_spec (K I) (K I) Locale.cert_expr;
   1.255 +
   1.256 +fun gen_class prep_spec prep_param local_syntax bname
   1.257 +    raw_supclasses raw_includes_elems raw_other_consts thy =
   1.258 +  let
   1.259 +    val (((sups, supconsts), (supsort, mergeexpr)), elems) =
   1.260 +      prep_spec thy raw_supclasses raw_includes_elems;
   1.261 +    val other_consts = map (prep_param thy) raw_other_consts;
   1.262      fun mk_instT class = Symtab.empty
   1.263        |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class]));
   1.264      fun mk_inst class param_names cs =
   1.265        Symtab.empty
   1.266        |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
   1.267             (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
   1.268 -    (*FIXME need proper concept for reading locale statements*)
   1.269 -    fun subst_classtyvar (_, _) =
   1.270 -          TFree (AxClass.param_tyvarname, [])
   1.271 -      | subst_classtyvar (v, sort) =
   1.272 -          error ("Sort constraint illegal in type class, for type variable "
   1.273 -            ^ v ^ "::" ^ Sign.string_of_sort thy sort);
   1.274 -    (*val subst_classtyvars = Element.map_ctxt {name = I, var = I, term = I,
   1.275 -      typ = Term.map_type_tfree subst_classtyvar, fact = I, attrib = I};*)
   1.276 -    val other_consts = map (prep_param thy) raw_other_consts;
   1.277 -    val (elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
   1.278 -      | Locale.Expr i => apsnd (cons i)) raw_elems ([], []);
   1.279 -    val supclasses = map (prep_class thy) raw_supclasses;
   1.280 -    val sups = filter (is_some o lookup_class_data thy) supclasses
   1.281 -      |> Sign.minimize_sort thy;
   1.282 -    val supsort = Sign.minimize_sort thy supclasses;
   1.283 -    val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups;
   1.284 -    val supexpr = Locale.Merge (suplocales @ includes);
   1.285 -    val supparams = (map fst o Locale.parameters_of_expr thy)
   1.286 -      (Locale.Merge suplocales);
   1.287 -    val supconsts = AList.make (the o AList.lookup (op =) (params_of_sort thy sups))
   1.288 -      (map fst supparams);
   1.289 -    (*val elems_constrains = map
   1.290 -      (Element.Constrains o apsnd (Term.map_type_tfree subst_classtyvar)) supparams;*)
   1.291 -    fun mk_tyvar (_, sort) = TFree (AxClass.param_tyvarname,
   1.292 -      if Sign.subsort thy (supsort, sort) then sort else error
   1.293 -        ("Sort " ^ Sign.string_of_sort thy sort
   1.294 -          ^ " is less general than permitted least general sort "
   1.295 -          ^ Sign.string_of_sort thy supsort));
   1.296      fun extract_params thy name_locale =
   1.297        let
   1.298          val params = Locale.parameters_of thy name_locale;
   1.299 -        val v = case (maps typ_tfrees o map (snd o fst)) params
   1.300 -         of (v, _) :: _ => v
   1.301 -          | [] => AxClass.param_tyvarname;
   1.302 +        val local_sort = case AList.group (op =) ((maps typ_tfrees o map (snd o fst)) params)
   1.303 +         of [(_, local_sort :: _)] => local_sort
   1.304 +          | _ => Sign.defaultS thy
   1.305 +          | vs => error ("exactly one type variable required: " ^ commas (map fst vs));
   1.306 +        val _ = if Sign.subsort thy (supsort, local_sort) then () else error
   1.307 +          ("Sort " ^ Sign.string_of_sort thy local_sort
   1.308 +            ^ " is less general than permitted least general sort "
   1.309 +            ^ Sign.string_of_sort thy supsort);
   1.310        in
   1.311 -        (v, (map fst params, params
   1.312 -        |> (map o apfst o apsnd o Term.map_type_tfree) mk_tyvar
   1.313 +        (local_sort, (map fst params, params
   1.314 +        |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, local_sort)))
   1.315          |> (map o apsnd) (fork_mixfix true NONE #> fst)
   1.316          |> chop (length supconsts)
   1.317          |> snd))
   1.318 @@ -620,19 +718,19 @@
   1.319        #> snd
   1.320    in
   1.321      thy
   1.322 -    |> add_locale (SOME "") bname supexpr ((*elems_constrains @*) elems)
   1.323 +    |> Locale.add_locale_i (SOME "") bname mergeexpr elems
   1.324      |-> (fn name_locale => ProofContext.theory_result (
   1.325        `(fn thy => extract_params thy name_locale)
   1.326 -      #-> (fn (v, (globals, params)) =>
   1.327 +      #-> (fn (local_sort, (globals, params)) =>
   1.328          AxClass.define_class_params (bname, supsort) params
   1.329            (extract_assumes name_locale params) other_consts
   1.330        #-> (fn (name_axclass, (consts, axioms)) =>
   1.331          `(fn thy => class_intro thy name_locale name_axclass sups)
   1.332        #-> (fn class_intro =>
   1.333          add_class_data ((name_axclass, sups),
   1.334 -          (name_locale, map fst params ~~ map fst consts, v,
   1.335 +          (name_locale, map fst params ~~ map fst consts, local_sort,
   1.336              (mk_instT name_axclass, mk_inst name_axclass (map fst globals)
   1.337 -              (map snd supconsts @ consts)), class_intro))
   1.338 +              (map snd supconsts @ consts)), class_intro, local_syntax))
   1.339        #> note_intro name_axclass class_intro
   1.340        #> class_interpretation name_axclass axioms []
   1.341        #> pair name_axclass
   1.342 @@ -641,18 +739,12 @@
   1.343  
   1.344  in
   1.345  
   1.346 -val class_cmd = gen_class Locale.add_locale Sign.intern_class read_param;
   1.347 -val class = gen_class Locale.add_locale_i Sign.certify_class (K I);
   1.348 +val class_cmd = gen_class read_class_spec read_param;
   1.349 +val class = gen_class check_class_spec (K I);
   1.350  
   1.351  end; (*local*)
   1.352  
   1.353  
   1.354 -(* class target context *)
   1.355 -
   1.356 -fun remove_constraints class thy =
   1.357 -  thy |> fold_map (get_remove_contraint o fst) (these_localized thy class);
   1.358 -
   1.359 -
   1.360  (* definition in class target *)
   1.361  
   1.362  fun export_fixes thy class =
   1.363 @@ -673,11 +765,10 @@
   1.364          val n2 = NameSpace.qualifier n1;
   1.365          val n3 = NameSpace.base n1;
   1.366        in NameSpace.implode [n2, prfx, n3] end;
   1.367 -    val v = (#v o the_class_data thy) class;
   1.368      val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) [class];
   1.369 +    val rhs' = export_fixes thy class rhs;
   1.370      val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
   1.371 -      if w = v then TFree (w, constrain_sort sort) else TFree var);
   1.372 -    val rhs' = export_fixes thy class rhs;
   1.373 +      if w = AxClass.param_tyvarname then TFree (w, constrain_sort sort) else TFree var);
   1.374      val ty' = Term.fastype_of rhs';
   1.375      val ty'' = subst_typ ty';
   1.376      val c' = mk_name c;
   1.377 @@ -688,7 +779,7 @@
   1.378          val def' = symmetric def;
   1.379          val def_eq = Thm.prop_of def';
   1.380          val typargs = Sign.const_typargs thy (c', fastype_of rhs);
   1.381 -        val typidx = find_index (fn TFree (w, _) => v = w | _ => false) typargs;
   1.382 +        val typidx = find_index (fn TFree (w, _) => AxClass.param_tyvarname = w | _ => false) typargs;
   1.383        in
   1.384          thy
   1.385          |> class_interpretation class [def'] [def_eq]
   1.386 @@ -754,52 +845,4 @@
   1.387  
   1.388  end; (*local*)
   1.389  
   1.390 -(*experimental*)
   1.391 -fun class_term_check thy class =
   1.392 -  let
   1.393 -    val algebra = Sign.classes_of thy;
   1.394 -    val { v, ... } = the_class_data thy class;
   1.395 -    fun add_constrain_classtyp sort' (ty as TFree (v, _)) =
   1.396 -          AList.map_default (op =) (v, []) (curry (Sorts.inter_sort algebra) sort')
   1.397 -      | add_constrain_classtyp sort' (Type (tyco, tys)) = case Sorts.mg_domain algebra tyco sort'
   1.398 -         of sorts => fold2 add_constrain_classtyp sorts tys;
   1.399 -    fun class_arg c idx ty =
   1.400 -      let
   1.401 -        val typargs = Sign.const_typargs thy (c, ty);
   1.402 -        fun classtyp (t as TFree (w, _)) = if w = v then NONE else SOME t
   1.403 -          | classtyp t = SOME t;
   1.404 -      in classtyp (nth typargs idx) end;
   1.405 -    fun add_inst (c, ty) (terminsts, typinsts) = case local_param thy class c
   1.406 -     of NONE => (terminsts, typinsts)
   1.407 -      | SOME (t, (class', idx)) => (case class_arg c idx ty
   1.408 -         of NONE => (((c, ty), t) :: terminsts, typinsts)
   1.409 -          | SOME ty => (terminsts, add_constrain_classtyp [class'] ty typinsts));
   1.410 -  in pair o (fn ts => let
   1.411 -    val cs = (fold o fold_aterms) (fn Const c_ty => insert (op =) c_ty | _ => I) ts [];
   1.412 -    val (terminsts, typinsts) = fold add_inst cs ([], []);
   1.413 -  in
   1.414 -    ts
   1.415 -    |> (map o map_aterms) (fn t as Const c_ty => the_default t (AList.lookup (op =) terminsts c_ty)
   1.416 -         | t => t)
   1.417 -    |> (map o map_types o map_atyps) (fn t as TFree (v, sort) =>
   1.418 -         case AList.lookup (op =) typinsts v
   1.419 -          of SOME sort' => TFree (v, Sorts.inter_sort algebra (sort, sort'))
   1.420 -           | NONE => t)
   1.421 -  end) end;
   1.422 -
   1.423 -val init_ref = ref (K (pair I) : class -> Proof.context -> (theory -> theory) * Proof.context);
   1.424 -fun init class = ! init_ref class;
   1.425 -
   1.426 -fun init_default class ctxt =
   1.427 -  let
   1.428 -    val thy = ProofContext.theory_of ctxt;
   1.429 -    val term_check = class_term_check thy class;
   1.430 -  in
   1.431 -    ctxt
   1.432 -    (*|> ProofContext.theory_result (remove_constraints class)*)
   1.433 -    |> Context.proof_map (Syntax.add_term_check term_check)
   1.434 -    (*|>> fold (fn (c, ty) => Sign.add_const_constraint_i (c, SOME ty))*)
   1.435 -    |> pair I
   1.436 -  end;
   1.437 -
   1.438  end;