--- a/src/HOL/Modelcheck/mucke_oracle.ML Fri Jun 17 18:33:13 2005 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Fri Jun 17 18:33:14 2005 +0200
@@ -984,8 +984,8 @@
val s = post_last_dot(fst(qtn a));
fun param_types ((Const("Trueprop",_)) $ (_ $ (Var(_,Type(_,t))))) = t |
param_types _ = error "malformed induct-theorem in preprocess_td";
- val pl = param_types (concl_of (get_thm (theory_of_sign sg) (s ^ ".induct", NONE)));
- val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm (theory_of_sign sg) (s ^ ".induct", NONE)));
+ val pl = param_types (concl_of (get_thm sg (s ^ ".induct", NONE)));
+ val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm sg (s ^ ".induct", NONE)));
val ntl = new_types l;
in
((a,l) :: (preprocess_td sg (ntl @ b) (a :: done)))