src/HOL/Modelcheck/mucke_oracle.ML

--- a/src/HOL/Modelcheck/mucke_oracle.ML	Wed Apr 04 20:22:32 2007 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Wed Apr 04 23:29:33 2007 +0200
@@ -96,7 +96,7 @@
 in
 
 fun if_full_simp_tac sset i state =
-let val sign = #sign (rep_thm state);
+let val sign = Thm.theory_of_thm state;
         val (subgoal::_) = Library.drop(i-1,prems_of state);
         val prems = Logic.strip_imp_prems subgoal;
 	val concl = Logic.strip_imp_concl subgoal;