# HG changeset patch
# User wenzelm
# Date 1194548887 -3600
# Node ID 24d1568af397b21dc3dbc3358d8f5c07b95798d7
# Parent  bf84dff3280dc55593095f9d0cbc898663a1b0dd
discontinued legacy vars;

diff -r bf84dff3280d -r 24d1568af397 src/Pure/Isar/constdefs.ML
--- 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;