--- a/src/Pure/Isar/constdefs.ML Thu Nov 08 20:08:02 2007 +0100
+++ b/src/Pure/Isar/constdefs.ML Thu Nov 08 20:08:07 2007 +0100
@@ -34,7 +34,7 @@
NONE => ((NONE, NoSyn), struct_ctxt)
| SOME raw_var =>
struct_ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] =>
- ProofContext.add_fixes_legacy [(x, T, mx)] #> snd #> pair (SOME x, mx)));
+ ProofContext.add_fixes_i [(x, T, mx)] #> snd #> pair (SOME x, mx)));
val prop = prep_prop var_ctxt raw_prop;
val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
@@ -61,7 +61,7 @@
val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy;
in Pretty.writeln (ProofDisplay.pretty_consts ctxt (K true) decls); thy' end;
-val add_constdefs = gen_constdefs ProofContext.read_vars_legacy Syntax.read_prop Attrib.attribute;
-val add_constdefs_i = gen_constdefs ProofContext.cert_vars_legacy ProofContext.cert_prop (K I);
+val add_constdefs = gen_constdefs ProofContext.read_vars Syntax.read_prop Attrib.attribute;
+val add_constdefs_i = gen_constdefs ProofContext.cert_vars ProofContext.cert_prop (K I);
end;