# HG changeset patch
# User haftmann
# Date 1160464638 -7200
# Node ID e65e1234c9d3037a623e17fdaa0e337609823ad4
# Parent  19d9b78218fd5c42575c74d24450a0676fcba127
fixed typo

diff -r 19d9b78218fd -r e65e1234c9d3 src/HOL/simpdata.ML
--- 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")))));