canonical interpretation interface
authorhaftmann
Mon Oct 15 15:29:43 2007 +0200 (2007-10-15)
changeset 25038522abf8a5f87
parent 25037 d6a3dec2375d
child 25039 06ed511837d5
canonical interpretation interface
src/Pure/Isar/class.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/class.ML	Mon Oct 15 15:29:41 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Mon Oct 15 15:29:43 2007 +0200
     1.3 @@ -19,11 +19,12 @@
     1.4    val class_cmd: bstring -> xstring list -> Element.context Locale.element list
     1.5      -> xstring list -> theory -> string * Proof.context
     1.6    val init: class -> Proof.context -> Proof.context;
     1.7 -  val add_const_in_class: string -> (string * mixfix) * term -> theory -> string * theory
     1.8 -  val add_abbrev_in_class: string -> Syntax.mode -> (string * mixfix) * term -> theory ->
     1.9 -    string * theory
    1.10 +  val add_const_in_class: string -> (string * mixfix) * (string * term)
    1.11 +    -> theory -> string * theory
    1.12 +  val add_abbrev_in_class: string -> Syntax.mode -> (string * mixfix) * (string * term)
    1.13 +    -> theory -> string * theory
    1.14    val remove_constraint: class -> string -> Proof.context -> Proof.context
    1.15 -  val is_class: theory -> string -> bool
    1.16 +  val is_class: theory -> class -> bool
    1.17    val these_params: theory -> sort -> (string * (string * typ)) list
    1.18    val intro_classes_tac: thm list -> tactic
    1.19    val default_intro_classes_tac: thm list -> tactic
    1.20 @@ -83,6 +84,15 @@
    1.21        | NONE => thm;
    1.22    in strip end;
    1.23  
    1.24 +fun get_remove_global_constraint c thy =
    1.25 +  let
    1.26 +    val ty = Sign.the_const_constraint thy c;
    1.27 +  in
    1.28 +    thy
    1.29 +    |> Sign.add_const_constraint (c, NONE)
    1.30 +    |> pair (c, Logic.unvarifyT ty)
    1.31 +  end;
    1.32 +
    1.33  
    1.34  (** axclass command **)
    1.35  
    1.36 @@ -232,14 +242,6 @@
    1.37       of [] => ()
    1.38        | dupl_tycos => error ("Type constructors occur more than once in arities: "
    1.39            ^ commas_quote dupl_tycos);
    1.40 -    fun get_remove_constraint c thy =
    1.41 -      let
    1.42 -        val ty = Sign.the_const_constraint thy c;
    1.43 -      in
    1.44 -        thy
    1.45 -        |> Sign.add_const_constraint (c, NONE)
    1.46 -        |> pair (c, Logic.unvarifyT ty)
    1.47 -      end;
    1.48      fun get_consts_class tyco ty class =
    1.49        let
    1.50          val cs = (these o try (#params o AxClass.get_info theory)) class;
    1.51 @@ -283,7 +285,7 @@
    1.52        #> after_qed defs;
    1.53    in
    1.54      theory
    1.55 -    |> fold_map get_remove_constraint (map fst cs |> distinct (op =))
    1.56 +    |> fold_map get_remove_global_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 @@ -311,12 +313,11 @@
    1.61  (** class data **)
    1.62  
    1.63  datatype class_data = ClassData of {
    1.64 -  locale: string,
    1.65    consts: (string * string) list
    1.66      (*locale parameter ~> constant name*),
    1.67    local_sort: sort,
    1.68 -  inst: typ Symtab.table * term Symtab.table
    1.69 -    (*canonical interpretation*),
    1.70 +  inst: (typ option list * term option list) * term Symtab.table
    1.71 +    (*canonical interpretation FIXME*),
    1.72    intro: thm,
    1.73    defs: thm list,
    1.74    operations: (string * (term * (typ * int))) list
    1.75 @@ -326,50 +327,46 @@
    1.76  };
    1.77  
    1.78  fun rep_class_data (ClassData d) = d;
    1.79 -fun mk_class_data ((locale, consts, local_sort, inst, intro),
    1.80 +fun mk_class_data ((consts, local_sort, inst, intro),
    1.81      (defs, operations, operations_rev)) =
    1.82 -  ClassData { locale = locale, consts = consts, local_sort = local_sort, inst = inst,
    1.83 +  ClassData { consts = consts, local_sort = local_sort, inst = inst,
    1.84      intro = intro, defs = defs, operations = operations,
    1.85      operations_rev = operations_rev };
    1.86 -fun map_class_data f (ClassData { locale, consts, local_sort, inst, intro,
    1.87 +fun map_class_data f (ClassData { consts, local_sort, inst, intro,
    1.88      defs, operations, operations_rev }) =
    1.89 -  mk_class_data (f ((locale, consts, local_sort, inst, intro),
    1.90 +  mk_class_data (f ((consts, local_sort, inst, intro),
    1.91      (defs, operations, operations_rev)));
    1.92 -fun merge_class_data _ (ClassData { locale = locale, consts = consts,
    1.93 +fun merge_class_data _ (ClassData { consts = consts,
    1.94      local_sort = local_sort, inst = inst, intro = intro,
    1.95      defs = defs1, operations = operations1, operations_rev = operations_rev1 },
    1.96 -  ClassData { locale = _, consts = _, local_sort = _, inst = _, intro = _,
    1.97 +  ClassData { consts = _, local_sort = _, inst = _, intro = _,
    1.98      defs = defs2, operations = operations2, operations_rev = operations_rev2 }) =
    1.99 -  mk_class_data ((locale, consts, local_sort, inst, intro),
   1.100 +  mk_class_data ((consts, local_sort, inst, intro),
   1.101      (Thm.merge_thms (defs1, defs2),
   1.102        AList.merge (op =) (K true) (operations1, operations2),
   1.103        AList.merge (op =) (K true) (operations_rev1, operations_rev2)));
   1.104  
   1.105 -fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));
   1.106 -
   1.107  structure ClassData = TheoryDataFun
   1.108  (
   1.109 -  type T = class_data Graph.T * class Symtab.table
   1.110 -    (*locale name ~> class name*);
   1.111 -  val empty = (Graph.empty, Symtab.empty);
   1.112 +  type T = class_data Graph.T
   1.113 +  val empty = Graph.empty;
   1.114    val copy = I;
   1.115    val extend = I;
   1.116 -  fun merge _ = merge_pair (Graph.join merge_class_data) (Symtab.merge (K true));
   1.117 +  fun merge _ = Graph.join merge_class_data;
   1.118  );
   1.119  
   1.120  
   1.121  (* queries *)
   1.122  
   1.123 -val is_class = Symtab.defined o snd o ClassData.get;
   1.124 -
   1.125 -val lookup_class_data = Option.map rep_class_data oo try o Graph.get_node
   1.126 -  o fst o ClassData.get;
   1.127 +val lookup_class_data = Option.map rep_class_data oo try o Graph.get_node o ClassData.get;
   1.128  
   1.129  fun the_class_data thy class = case lookup_class_data thy class
   1.130   of NONE => error ("Undeclared class " ^ quote class)
   1.131    | SOME data => data;
   1.132  
   1.133 -val ancestry = Graph.all_succs o fst o ClassData.get;
   1.134 +val is_class = is_some oo lookup_class_data;
   1.135 +
   1.136 +val ancestry = Graph.all_succs o ClassData.get;
   1.137  
   1.138  fun these_params thy =
   1.139    let
   1.140 @@ -386,7 +383,7 @@
   1.141  
   1.142  fun these_intros thy =
   1.143    Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_class_data) data))
   1.144 -    ((fst o ClassData.get) thy) [];
   1.145 +    (ClassData.get thy) [];
   1.146  
   1.147  fun these_operations thy =
   1.148    maps (#operations o the_class_data thy) o ancestry thy;
   1.149 @@ -428,7 +425,7 @@
   1.150        (SOME o Pretty.str) ("class " ^ class ^ ":"),
   1.151        (SOME o Pretty.block) [Pretty.str "supersort: ",
   1.152          (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
   1.153 -      Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class),
   1.154 +      if is_class thy class then (SOME o Pretty.str) ("locale: " ^ class) else NONE,
   1.155        ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
   1.156          o these o Option.map #params o try (AxClass.get_info thy)) class,
   1.157        (SOME o Pretty.block o Pretty.breaks) [
   1.158 @@ -444,21 +441,29 @@
   1.159  
   1.160  (* updaters *)
   1.161  
   1.162 -fun add_class_data ((class, superclasses), (locale, cs, local_sort, inst, intro)) =
   1.163 +fun add_class_data ((class, superclasses), (cs, local_sort, inst, intro)) thy =
   1.164    let
   1.165 +    (*FIXME*)
   1.166 +    val is_empty = null (fold (fn ((_, ty), _) => fold_atyps cons ty) cs [])
   1.167 +      andalso null ((fold o fold_types o fold_atyps) cons
   1.168 +        (maps snd (Locale.global_asms_of thy class)) []);
   1.169 +    (*FIXME*)
   1.170 +    val inst_params = map
   1.171 +      (SOME o the o Symtab.lookup inst o fst o fst)
   1.172 +        (Locale.parameters_of_expr thy (Locale.Locale class));
   1.173 +    val instT = if is_empty then [] else [SOME (TFree (Name.aT, [class]))];
   1.174 +    val inst' = ((instT, inst_params), inst);
   1.175      val operations = map (fn (v_ty, (c, ty)) => (c, (Free v_ty, (ty, 0)))) cs;
   1.176      val cs = (map o pairself) fst cs;
   1.177 -    val add_class = Graph.new_node (class, mk_class_data ((locale,
   1.178 -          cs, local_sort, inst, intro),
   1.179 -            ([], operations, [])))
   1.180 +    val add_class = Graph.new_node (class,
   1.181 +        mk_class_data ((cs, local_sort, inst', intro), ([], operations, [])))
   1.182        #> fold (curry Graph.add_edge class) superclasses;
   1.183 -    val add_locale = Symtab.update (locale, class);
   1.184    in
   1.185 -    ClassData.map (fn (gr, tab) => (add_class gr, add_locale tab))
   1.186 +    ClassData.map add_class thy
   1.187    end;
   1.188  
   1.189  fun register_operation class (entry, some_def) =
   1.190 -  (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd)
   1.191 +  (ClassData.map o Graph.map_node class o map_class_data o apsnd)
   1.192      (fn (defs, operations, operations_rev) =>
   1.193        (case some_def of NONE => defs | SOME def => def :: defs,
   1.194          entry :: operations, (*FIXME*)operations_rev));
   1.195 @@ -468,13 +473,13 @@
   1.196  
   1.197  val class_prefix = Logic.const_of_class o Sign.base_name;
   1.198  
   1.199 -fun class_intro thy locale class sups =
   1.200 +fun class_intro thy class sups =
   1.201    let
   1.202      fun class_elim class =
   1.203        case (#axioms o AxClass.get_info thy) class
   1.204         of [thm] => SOME (Drule.unconstrainTs thm)
   1.205          | [] => NONE;
   1.206 -    val pred_intro = case Locale.intros thy locale
   1.207 +    val pred_intro = case Locale.intros thy class
   1.208       of ([ax_intro], [intro]) => intro |> OF_LAST ax_intro |> SOME
   1.209        | ([intro], []) => SOME intro
   1.210        | ([], [intro]) => SOME intro
   1.211 @@ -499,30 +504,17 @@
   1.212  
   1.213  fun class_interpretation class facts defs thy =
   1.214    let
   1.215 -    val inst = #inst (the_class_data thy class);
   1.216 +    val params = these_params thy [class];
   1.217 +    val { inst = ((_, inst), _), ... } = the_class_data thy class;
   1.218 +    (*val _ = tracing ("interpreting with " ^ cat_lines (map (setmp show_sorts true makestring)
   1.219 +      (map_filter I inst)));*)
   1.220      val tac = ALLGOALS (ProofContext.fact_tac facts);
   1.221 +    val prfx = class_prefix class;
   1.222    in
   1.223 -    prove_interpretation tac ((false, class_prefix class), []) (Locale.Locale class)
   1.224 -      (inst, defs) thy
   1.225 -  end;
   1.226 -
   1.227 -fun interpretation_in_rule thy (class1, class2) =
   1.228 -  let
   1.229 -    val ctxt = ProofContext.init thy;
   1.230 -    fun mk_axioms class =
   1.231 -      let
   1.232 -        val { locale, inst = (_, insttab), ... } = the_class_data thy class;
   1.233 -      in
   1.234 -        Locale.global_asms_of thy locale
   1.235 -        |> maps snd
   1.236 -        |> (map o map_aterms) (fn Free (s, _) => (the o Symtab.lookup insttab) s | t => t)
   1.237 -        |> (map o map_types o map_atyps) (fn TFree _ => TFree (Name.aT, [class1]) | T => T)
   1.238 -        |> map (ObjectLogic.ensure_propT thy)
   1.239 -      end;
   1.240 -    val (prems, concls) = pairself mk_axioms (class1, class2);
   1.241 -  in
   1.242 -    Goal.prove_global thy [] prems (Logic.mk_conjunction_list concls)
   1.243 -      (Locale.intro_locales_tac true ctxt)
   1.244 +    thy
   1.245 +    |> fold_map (get_remove_global_constraint o fst o snd) params
   1.246 +    ||> prove_interpretation tac ((false, prfx), []) (Locale.Locale class) (inst, defs)
   1.247 +    |-> (fn cs => fold (Sign.add_const_constraint o apsnd SOME) cs)
   1.248    end;
   1.249  
   1.250  fun intro_classes_tac facts st =
   1.251 @@ -643,7 +635,7 @@
   1.252      val supclasses = map (prep_class thy) raw_supclasses;
   1.253      val (sups, local_sort) = sups_local_sort thy supclasses;
   1.254      val supsort = Sign.minimize_sort thy supclasses;
   1.255 -    val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups;
   1.256 +    val suplocales = map Locale.Locale sups;
   1.257      val (raw_elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
   1.258        | Locale.Expr i => apsnd (cons (prep_expr thy i))) raw_includes_elems ([], []);
   1.259      val supexpr = Locale.Merge suplocales;
   1.260 @@ -695,18 +687,17 @@
   1.261  fun gen_class prep_spec prep_param bname
   1.262      raw_supclasses raw_includes_elems raw_other_consts thy =
   1.263    let
   1.264 +    val class = Sign.full_name thy bname;
   1.265      val (((sups, supconsts), (supsort, local_sort, mergeexpr)), elems) =
   1.266        prep_spec thy raw_supclasses raw_includes_elems;
   1.267      val other_consts = map (tap (Sign.the_const_type thy) o prep_param thy) raw_other_consts;
   1.268 -    fun mk_instT class = Symtab.empty
   1.269 -      |> Symtab.update (Name.aT, TFree (Name.aT, [class]));
   1.270      fun mk_inst class param_names cs =
   1.271        Symtab.empty
   1.272        |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
   1.273             (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
   1.274 -    fun extract_params thy name_locale =
   1.275 +    fun extract_params thy =
   1.276        let
   1.277 -        val params = Locale.parameters_of thy name_locale;
   1.278 +        val params = Locale.parameters_of thy class;
   1.279          val _ = if Sign.subsort thy (supsort, local_sort) then () else error
   1.280            ("Sort " ^ Sign.string_of_sort thy local_sort
   1.281              ^ " is less general than permitted least general sort "
   1.282 @@ -718,7 +709,7 @@
   1.283          |> chop (length supconsts)
   1.284          |> snd)
   1.285        end;
   1.286 -    fun extract_assumes name_locale params thy cs =
   1.287 +    fun extract_assumes params thy cs =
   1.288        let
   1.289          val consts = supconsts @ (map (fst o fst) params ~~ cs);
   1.290          fun subst (Free (c, ty)) =
   1.291 @@ -728,32 +719,32 @@
   1.292            ((Sign.base_name name, map (Attrib.attribute_i thy) atts),
   1.293              (map o map_aterms) subst ts);
   1.294        in
   1.295 -        Locale.global_asms_of thy name_locale
   1.296 +        Locale.global_asms_of thy class
   1.297          |> map prep_asm
   1.298        end;
   1.299 -    fun note_intro name_axclass class_intro =
   1.300 -      PureThy.note_thmss_qualified "" (class_prefix name_axclass)
   1.301 +    fun note_intro class_intro =
   1.302 +      PureThy.note_thmss_qualified "" (class_prefix class)
   1.303          [(("intro", []), [([class_intro], [])])]
   1.304        #> snd
   1.305    in
   1.306      thy
   1.307      |> Locale.add_locale_i (SOME "") bname mergeexpr elems
   1.308 -    |-> (fn name_locale => ProofContext.theory_result (
   1.309 -      `(fn thy => extract_params thy name_locale)
   1.310 +    |> snd
   1.311 +    |> ProofContext.theory (`extract_params
   1.312        #-> (fn (globals, params) =>
   1.313          define_class_params (bname, supsort) params
   1.314 -          (extract_assumes name_locale params) other_consts
   1.315 -      #-> (fn (name_axclass, (consts, axioms)) =>
   1.316 -        `(fn thy => class_intro thy name_locale name_axclass sups)
   1.317 +          (extract_assumes params) other_consts
   1.318 +      #-> (fn (_, (consts, axioms)) =>
   1.319 +        `(fn thy => class_intro thy class sups)
   1.320        #-> (fn class_intro =>
   1.321 -        add_class_data ((name_axclass, sups),
   1.322 -          (name_locale, map fst params ~~ consts, local_sort,
   1.323 -            (mk_instT name_axclass, mk_inst name_axclass (map fst globals)
   1.324 -              (map snd supconsts @ consts)), class_intro))
   1.325 -      #> note_intro name_axclass class_intro
   1.326 -      #> class_interpretation name_axclass axioms []
   1.327 -      #> pair name_axclass
   1.328 -      )))))
   1.329 +        add_class_data ((class, sups),
   1.330 +          (map fst params ~~ consts, local_sort,
   1.331 +            mk_inst class (map fst globals) (map snd supconsts @ consts),
   1.332 +              class_intro))
   1.333 +      #> note_intro class_intro
   1.334 +      #> class_interpretation class axioms []
   1.335 +      ))))
   1.336 +    |> pair class
   1.337    end;
   1.338  
   1.339  in
   1.340 @@ -782,8 +773,9 @@
   1.341      val typidx = find_index (fn TFree (w, _) => Name.aT = w | _ => false) typargs;
   1.342    in (c, (rhs, (ty, typidx))) end;
   1.343  
   1.344 -fun add_const_in_class class ((c, mx), rhs) thy =
   1.345 +fun add_const_in_class class ((c, mx), (c_loc, rhs)) thy =
   1.346    let
   1.347 +    val _ = tracing c_loc;
   1.348      val prfx = class_prefix class;
   1.349      val thy' = thy |> Sign.add_path prfx;
   1.350  
   1.351 @@ -793,6 +785,7 @@
   1.352      val ty' = Term.fastype_of rhs';
   1.353      val ty'' = subst_typ ty';
   1.354      val c' = Sign.full_name thy' c;
   1.355 +    val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c;
   1.356      val def = (c, Logic.mk_equals (Const (c', ty'), rhs'));
   1.357      val (mx', _) = fork_mixfix true true mx;
   1.358      fun interpret def thy =
   1.359 @@ -808,6 +801,7 @@
   1.360        end;
   1.361    in
   1.362      thy'
   1.363 +    |> Sign.hide_consts_i false [c'']
   1.364      |> Sign.declare_const [] (c, ty', mx') |> snd
   1.365      |> Sign.parent_path
   1.366      |> Sign.sticky_prefix prfx
   1.367 @@ -820,10 +814,12 @@
   1.368  
   1.369  (* abbreviation in class target *)
   1.370  
   1.371 -fun add_abbrev_in_class class prmode ((c, mx), rhs) thy =
   1.372 +fun add_abbrev_in_class class prmode ((c, mx), (c_loc, rhs)) thy =
   1.373    let
   1.374 +    val _ = tracing c_loc;
   1.375      val prfx = class_prefix class;
   1.376 -    val naming = Sign.naming_of thy |> NameSpace.add_path prfx |> NameSpace.add_path prfx; (* FIXME !? *)
   1.377 +    val naming = Sign.naming_of thy |> NameSpace.add_path prfx |> NameSpace.add_path prfx;
   1.378 +      (*FIXME*)
   1.379      val c' = NameSpace.full naming c;
   1.380      val rhs' = export_fixes thy class rhs;
   1.381      val ty' = Term.fastype_of rhs';
     2.1 --- a/src/Pure/Isar/locale.ML	Mon Oct 15 15:29:41 2007 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Mon Oct 15 15:29:43 2007 +0200
     2.3 @@ -99,7 +99,7 @@
     2.4  
     2.5    val interpretation_i: (Proof.context -> Proof.context) ->
     2.6      (bool * string) * Attrib.src list -> expr ->
     2.7 -    (typ Symtab.table * term Symtab.table) * term list ->
     2.8 +    term option list * term list ->
     2.9      theory -> Proof.state
    2.10    val interpretation: (Proof.context -> Proof.context) ->
    2.11      (bool * string) * Attrib.src list -> expr ->
    2.12 @@ -109,7 +109,7 @@
    2.13      xstring * expr -> theory -> Proof.state
    2.14    val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
    2.15      (bool * string) * Attrib.src list -> expr ->
    2.16 -    (typ Symtab.table * term Symtab.table) * term list ->
    2.17 +    term option list * term list ->
    2.18      bool -> Proof.state -> Proof.state
    2.19    val interpret: (Proof.state -> Proof.state Seq.seq) ->
    2.20      (bool * string) * Attrib.src list -> expr ->
    2.21 @@ -2077,14 +2077,22 @@
    2.22        add_local_equation
    2.23        x;
    2.24  
    2.25 -fun prep_instantiations parse_term parse_prop ctxt parms (insts, eqns) =
    2.26 +fun prep_instantiations prep_term prep_prop ctxt parms (insts, eqns) =
    2.27    let
    2.28      (* parameters *)
    2.29      val (parm_names, parm_types) = parms |> split_list
    2.30        ||> map (TypeInfer.paramify_vars o Logic.varifyT);
    2.31 -    val type_parms = fold Term.add_tvarsT parm_types [] |> map TVar;
    2.32 +    val type_parms = fold Term.add_tvarsT parm_types [] |> map (Logic.mk_type o TVar);
    2.33      val type_parm_names = fold Term.add_tfreesT (map snd parms) [] |> map fst;
    2.34  
    2.35 +    (*(* type instantiations *)
    2.36 +    val dT = length type_parms - length instsT;
    2.37 +    val instsT =
    2.38 +      if dT < 0 then error "More type arguments than type parameters in instantiation."
    2.39 +      else instsT @ replicate dT NONE;
    2.40 +    val type_terms = map2 (fn t => fn SOME T => TypeInfer.constrain (Term.itselfT T) t
    2.41 +      | NONE => t) type_parms instsT;*)
    2.42 +
    2.43      (* parameter instantiations *)
    2.44      val d = length parms - length insts;
    2.45      val insts =
    2.46 @@ -2098,12 +2106,12 @@
    2.47      val (given_parm_names, given_parm_types) = given_ps |> split_list;
    2.48  
    2.49      (* prepare insts / eqns *)
    2.50 -    val given_insts' = map (parse_term ctxt) given_insts;
    2.51 -    val eqns' = map (parse_prop ctxt) eqns;
    2.52 +    val given_insts' = map (prep_term ctxt) given_insts;
    2.53 +    val eqns' = map (prep_prop ctxt) eqns;
    2.54  
    2.55      (* infer types *)
    2.56      val res = Syntax.check_terms ctxt
    2.57 -      (map Logic.mk_type type_parms @
    2.58 +      (type_parms @
    2.59         map2 TypeInfer.constrain given_parm_types given_insts' @
    2.60         eqns');
    2.61      val ctxt' = ctxt |> fold Variable.auto_fixes res;
    2.62 @@ -2116,9 +2124,8 @@
    2.63      val standard = Variable.export_morphism ctxt' ctxt;
    2.64    in ((instT, inst), eqns'') end;
    2.65  
    2.66 -
    2.67  val read_instantiations = prep_instantiations Syntax.parse_term Syntax.parse_prop;
    2.68 -val check_instantiations = prep_instantiations (K I) (K I);
    2.69 +val cert_instantiations = prep_instantiations (K I) (K I);
    2.70  
    2.71  fun gen_prep_registration mk_ctxt test_reg activate
    2.72      prep_attr prep_expr prep_insts
    2.73 @@ -2200,21 +2207,13 @@
    2.74  
    2.75  val prep_global_registration = gen_prep_global_registration
    2.76    Attrib.intern_src intern_expr read_instantiations;
    2.77 -(* FIXME: NEW
    2.78  val prep_global_registration_i = gen_prep_global_registration
    2.79 -  (K I) (K I) check_instantiations;
    2.80 -*)
    2.81 -val prep_global_registration_i = gen_prep_global_registration
    2.82 -  (K I) (K I) ((K o K) I);
    2.83 +  (K I) (K I) cert_instantiations;
    2.84  
    2.85  val prep_local_registration = gen_prep_local_registration
    2.86    Attrib.intern_src intern_expr read_instantiations;
    2.87 -(* FIXME: NEW
    2.88  val prep_local_registration_i = gen_prep_local_registration
    2.89 -  (K I) (K I) check_instantiations;
    2.90 -*)
    2.91 -val prep_local_registration_i = gen_prep_local_registration
    2.92 -  (K I) (K I) ((K o K) I);
    2.93 +  (K I) (K I) cert_instantiations;
    2.94  
    2.95  fun prep_registration_in_locale target expr thy =
    2.96    (* target already in internal form *)