# HG changeset patch
# User wenzelm
# Date 1194450179 -3600
# Node ID c65608a84919b190240cd4dbc027fbbb25ffba9b
# Parent  e417a723612569f970ba64e7e439ecd766a48688
discontinued ProofContext.read_prop_legacy;

diff -r e417a7236125 -r c65608a84919 src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Wed Nov 07 16:42:58 2007 +0100
+++ b/src/Pure/Isar/constdefs.ML	Wed Nov 07 16:42:59 2007 +0100
@@ -61,8 +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
-  ProofContext.read_prop_legacy Attrib.attribute;
+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);
 
 end;