--- a/src/HOL/simpdata.ML Tue Oct 10 09:17:17 2006 +0200
+++ b/src/HOL/simpdata.ML Tue Oct 10 09:17:18 2006 +0200
@@ -276,9 +276,9 @@
else error "Conclusion of congruence rules must be =-equality"
end);
-(* Elimination of True from asumptions: *)
+(* Elimination of True from assumptions: *)
-local fun rd s = read_cterm (sign_of (the_context())) (s, propT);
+local fun rd s = read_cterm (the_context()) (s, propT);
in val True_implies_equals = standard' (equal_intr
(implies_intr_hyps (implies_elim (assume (rd "True ==> PROP P")) TrueI))
(implies_intr_hyps (implies_intr (rd "True") (assume (rd "PROP P")))));