1.1 --- a/src/Pure/Isar/locale.ML	Wed Oct 10 10:50:11 2007 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Wed Oct 10 10:55:37 2007 +0200
     1.3 @@ -2107,45 +2107,48 @@
     1.4        add_local_equation
     1.5        x;
     1.6  
     1.7 -fun read_termT ctxt (t, T) =
     1.8 -  Syntax.parse_term ctxt t |> TypeInfer.constrain (TypeInfer.paramify_vars T);
     1.9 -
    1.10 -fun read_instantiations ctxt parms (insts, eqns) =
    1.11 +fun prep_instantiations parse_term parse_prop ctxt parms (insts, eqns) =
    1.12    let
    1.13 -    val thy = ProofContext.theory_of ctxt;
    1.14 +    (* parameters *)
    1.15 +    val (parm_names, parm_types) = parms |> split_list
    1.16 +      ||> map (TypeInfer.paramify_vars o Logic.varifyT);
    1.17 +    val type_parms = fold Term.add_tvarsT parm_types [] |> map TVar;
    1.18 +    val type_parm_names = fold Term.add_tfreesT (map snd parms) [] |> map fst;
    1.19  
    1.20      (* parameter instantiations *)
    1.21 -    val parms' = map (apsnd Logic.varifyT) parms;
    1.22      val d = length parms - length insts;
    1.23      val insts =
    1.24        if d < 0 then error "More arguments than parameters in instantiation."
    1.25        else insts @ replicate d NONE;
    1.26 -
    1.27 -    val given = (parms' ~~ insts) |> map_filter
    1.28 -      (fn (_, NONE) => NONE
    1.29 -        | ((x, T), SOME inst) => SOME (x, (inst, T)));
    1.30 -    val (given_ps, given_insts) = split_list given;
    1.31 -
    1.32 -    (* read given insts / eqns *)
    1.33 -    val all_vs = (map (read_termT ctxt) given_insts @ map (Syntax.read_prop ctxt) eqns)
    1.34 -      |> Syntax.check_terms ctxt;
    1.35 -    val ctxt' = ctxt |> fold Variable.declare_term all_vs;
    1.36 -    val (vs, eqns') = all_vs |> chop (length given_insts);
    1.37 -
    1.38 -    (* infer parameter types *)
    1.39 -    val tyenv = fold (fn ((_, T), t) => Sign.typ_match thy (T, Term.fastype_of t))
    1.40 -      (given_insts ~~ vs) Vartab.empty;
    1.41 -    val looseTs = fold (Term.add_tvarsT o Envir.typ_subst_TVars tyenv o #2) parms' [];
    1.42 -    val (fixedTs, _) = Variable.invent_types (map #2 looseTs) ctxt';
    1.43 -    val tyenv' =
    1.44 -      fold (fn ((xi, S), v) => Vartab.update_new (xi, (S, TFree v))) (looseTs ~~ fixedTs) tyenv;
    1.45 -
    1.46 -    (*results*)
    1.47 -    val instT = Vartab.fold (fn ((a, 0), (S, T)) =>
    1.48 -      if T = TFree (a, S) then I else Symtab.update (a, T)) tyenv' Symtab.empty;
    1.49 -    val inst = Symtab.make (given_ps ~~ vs);
    1.50 -  in ((instT, inst), eqns') end;
    1.51 -
    1.52 +    val (given_ps, given_insts) =
    1.53 +      ((parm_names ~~ parm_types) ~~ insts) |> map_filter
    1.54 +          (fn (_, NONE) => NONE
    1.55 +            | ((n, T), SOME inst) => SOME ((n, T), inst))
    1.56 +        |> split_list;
    1.57 +    val (given_parm_names, given_parm_types) = given_ps |> split_list;
    1.58 +
    1.59 +    (* prepare insts / eqns *)
    1.60 +    val given_insts' = map (parse_term ctxt) given_insts;
    1.61 +    val eqns' = map (parse_prop ctxt) eqns;
    1.62 +
    1.63 +    (* infer types *)
    1.64 +    val res = Syntax.check_terms ctxt
    1.65 +      (map Logic.mk_type type_parms @
    1.66 +       map (uncurry TypeInfer.constrain) (given_parm_types ~~ given_insts') @
    1.67 +       eqns');
    1.68 +    val ctxt' = ctxt |> fold Variable.auto_fixes res;
    1.69 +
    1.70 +    (* results *)
    1.71 +    val (type_parms'', res') = chop (length type_parms) res;
    1.72 +    val (given_insts'', eqns'') = chop (length given_insts) res';
    1.73 +    val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
    1.74 +    val inst = Symtab.make (given_parm_names ~~ given_insts'');
    1.75 +    val standard = Variable.export_morphism ctxt' ctxt;
    1.76 +  in ((instT, inst), eqns'') end;
    1.77 +
    1.78 +
    1.79 +val read_instantiations = prep_instantiations Syntax.parse_term Syntax.parse_prop;
    1.80 +val cert_instantiations = prep_instantiations Syntax.check_term Syntax.check_prop;
    1.81  
    1.82  fun gen_prep_registration mk_ctxt test_reg activate
    1.83      prep_attr prep_expr prep_insts
    1.84 @@ -2227,11 +2230,19 @@
    1.85  
    1.86  val prep_global_registration = gen_prep_global_registration
    1.87    Attrib.intern_src intern_expr read_instantiations;
    1.88 +(* FIXME: NEW
    1.89 +val prep_global_registration_i = gen_prep_global_registration
    1.90 +  (K I) (K I) cert_instantiations;
    1.91 +*)
    1.92  val prep_global_registration_i = gen_prep_global_registration
    1.93    (K I) (K I) ((K o K) I);
    1.94  
    1.95  val prep_local_registration = gen_prep_local_registration
    1.96    Attrib.intern_src intern_expr read_instantiations;
    1.97 +(* FIXME: NEW
    1.98 +val prep_local_registration_i = gen_prep_local_registration
    1.99 +  (K I) (K I) cert_instantiations;
   1.100 +*)
   1.101  val prep_local_registration_i = gen_prep_local_registration
   1.102    (K I) (K I) ((K o K) I);
   1.103