src/Pure/IsaPlanner/isand.ML

       (Term.term -> Thm.cterm) ->
       (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
   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) *)
   val fix_alls_in_term : Term.term -> Term.term * Term.term list
   val fix_alls_term : int -> Term.term -> Term.term * Term.term list