diff -r 86c73395c99b -r 932a50e2332f src/Pure/IsaPlanner/isand.ML
--- a/src/Pure/IsaPlanner/isand.ML	Sat Mar 11 17:30:35 2006 +0100
+++ b/src/Pure/IsaPlanner/isand.ML	Sat Mar 11 21:23:10 2006 +0100
@@ -56,7 +56,7 @@
   val allify_conditions' :
       (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
   val assume_allified :
-      Sign.sg -> (string * Term.sort) list * (string * Term.typ) list
+      theory -> (string * Term.sort) list * (string * Term.typ) list
       -> Term.term -> (Thm.cterm * Thm.thm)
 
   (* meta level fixed params (i.e. !! vars) *)