src/Pure/Isar/local_defs.ML
changeset 30763 6976521b4263
parent 30585 6b2ba4666336
child 31794 71af1fd6a5e4
     1.1 --- a/src/Pure/Isar/local_defs.ML	Sat Mar 28 17:21:49 2009 +0100
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Sat Mar 28 17:53:33 2009 +0100
     1.3 @@ -96,7 +96,7 @@
     1.4      val lhss = map (fst o Logic.dest_equals) eqs;
     1.5    in
     1.6      ctxt
     1.7 -    |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
     1.8 +    |> ProofContext.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
     1.9      |> fold Variable.declare_term eqs
    1.10      |> ProofContext.add_assms_i def_export
    1.11        (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
    1.12 @@ -115,7 +115,7 @@
    1.13      val T = Term.fastype_of rhs;
    1.14      val ([x'], ctxt') = ctxt
    1.15        |> Variable.declare_term rhs
    1.16 -      |> ProofContext.add_fixes_i [(x, SOME T, mx)];
    1.17 +      |> ProofContext.add_fixes [(x, SOME T, mx)];
    1.18      val lhs = Free (x', T);
    1.19      val _ = cert_def ctxt' (Logic.mk_equals (lhs, rhs));
    1.20      fun abbrev_export _ _ = (I, Envir.expand_term_frees [((x', T), rhs)]);