src/Pure/Isar/constdefs.ML
changeset 30763 6976521b4263
parent 30585 6b2ba4666336
child 32662 2faf1148c062
     1.1 --- a/src/Pure/Isar/constdefs.ML	Sat Mar 28 17:21:49 2009 +0100
     1.2 +++ b/src/Pure/Isar/constdefs.ML	Sat Mar 28 17:53:33 2009 +0100
     1.3 @@ -25,13 +25,13 @@
     1.4      fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
     1.5  
     1.6      val thy_ctxt = ProofContext.init thy;
     1.7 -    val struct_ctxt = #2 (ProofContext.add_fixes_i structs thy_ctxt);
     1.8 +    val struct_ctxt = #2 (ProofContext.add_fixes structs thy_ctxt);
     1.9      val ((d, mx), var_ctxt) =
    1.10        (case raw_decl of
    1.11          NONE => ((NONE, NoSyn), struct_ctxt)
    1.12        | SOME raw_var =>
    1.13            struct_ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] =>
    1.14 -            ProofContext.add_fixes_i [(x, T, mx)] #> snd #> pair (SOME x, mx)));
    1.15 +            ProofContext.add_fixes [(x, T, mx)] #> snd #> pair (SOME x, mx)));
    1.16  
    1.17      val prop = prep_prop var_ctxt raw_prop;
    1.18      val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));