# HG changeset patch
# User wenzelm
# Date 1213808100 -7200
# Node ID 042aebff17e19fa32119fecca8c179c9b25f095e
# Parent  121991a4884d539caea64584ef6b3feb96ce0346
OldGoals.read_prop;

diff -r 121991a4884d -r 042aebff17e1 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Jun 18 18:54:59 2008 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Wed Jun 18 18:55:00 2008 +0200
@@ -97,7 +97,7 @@
 val notTrueE = TrueI RSN (2, notE);
 val notFalseI = Seq.hd (atac 1 notI);
 val simp_thms' = map (fn s => mk_meta_eq (the (find_first
-  (equal (Sign.read_prop HOL.thy s) o prop_of) simp_thms)))
+  (equal (OldGoals.read_prop HOL.thy s) o prop_of) simp_thms)))
   ["(~True) = False", "(~False) = True",
    "(True --> ?P) = ?P", "(False --> ?P) = True",
    "(?P & True) = ?P", "(True & ?P) = ?P"];