1.1 --- a/src/Pure/Isar/locale.ML	Wed Oct 17 13:55:35 2007 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Wed Oct 17 13:55:37 2007 +0200
     1.3 @@ -2077,7 +2077,7 @@
     1.4        add_local_equation
     1.5        x;
     1.6  
     1.7 -fun prep_instantiations prep_term prep_prop ctxt parms (insts, eqns) =
     1.8 +fun prep_instantiations parse_term parse_prop ctxt parms (insts, eqns) =
     1.9    let
    1.10      (* parameters *)
    1.11      val (parm_names, parm_types) = parms |> split_list
    1.12 @@ -2105,11 +2105,11 @@
    1.13          |> split_list;
    1.14      val (given_parm_names, given_parm_types) = given_ps |> split_list;
    1.15  
    1.16 -    (* prepare insts / eqns *)
    1.17 -    val given_insts' = map (prep_term ctxt) given_insts;
    1.18 -    val eqns' = map (prep_prop ctxt) eqns;
    1.19 -
    1.20 -    (* infer types *)
    1.21 +    (* parse insts / eqns *)
    1.22 +    val given_insts' = map (parse_term ctxt) given_insts;
    1.23 +    val eqns' = map (parse_prop ctxt) eqns;
    1.24 +
    1.25 +    (* type inference etc. *)
    1.26      val res = Syntax.check_terms ctxt
    1.27        (type_parms @
    1.28         map2 TypeInfer.constrain given_parm_types given_insts' @
    1.29 @@ -2125,7 +2125,7 @@
    1.30    in ((instT, inst), eqns'') end;
    1.31  
    1.32  val read_instantiations = prep_instantiations Syntax.parse_term Syntax.parse_prop;
    1.33 -val cert_instantiations = prep_instantiations (K I) (K I);
    1.34 +val check_instantiations = prep_instantiations (K I) (K I);
    1.35  
    1.36  fun gen_prep_registration mk_ctxt test_reg activate
    1.37      prep_attr prep_expr prep_insts
    1.38 @@ -2208,12 +2208,12 @@
    1.39  val prep_global_registration = gen_prep_global_registration
    1.40    Attrib.intern_src intern_expr read_instantiations;
    1.41  val prep_global_registration_i = gen_prep_global_registration
    1.42 -  (K I) (K I) cert_instantiations;
    1.43 +  (K I) (K I) check_instantiations;
    1.44  
    1.45  val prep_local_registration = gen_prep_local_registration
    1.46    Attrib.intern_src intern_expr read_instantiations;
    1.47  val prep_local_registration_i = gen_prep_local_registration
    1.48 -  (K I) (K I) cert_instantiations;
    1.49 +  (K I) (K I) check_instantiations;
    1.50  
    1.51  fun prep_registration_in_locale target expr thy =
    1.52    (* target already in internal form *)