TFL/casesplit.ML

 fun casesplit_free fv i th =
     let
       val (subgoalth, exp) = IsaND.fix_alls i th;
       val subgoalth' = atomize_goals subgoalth;
       val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1);
-      val sgn = Thm.sign_of_thm th;
+      val sgn = Thm.theory_of_thm th;
 
       val splitter_thm = mk_casesplit_goal_thm sgn fv gt;
       val nsplits = Thm.nprems_of splitter_thm;
 
       val split_goal_th = splitter_thm RS subgoalth';

             handle Fail _ => NONE (* dest_skolem *)
           end;
       val (n,ty) = case Library.get_first getter freets
                 of SOME (n, ty) => (n, ty)
                  | _ => error ("no such variable " ^ vstr);
-      val sgn = Thm.sign_of_thm th;
+      val sgn = Thm.theory_of_thm th;
 
       val splitter_thm = mk_casesplit_goal_thm sgn (n,ty) gt;
       val nsplits = Thm.nprems_of splitter_thm;
 
       val split_goal_th = splitter_thm RS subgoalth';

 case split done during recdef's case analysis, this would avoid us
 having to (re)search for variables to split. *)
 fun splitto splitths genth =
     let
       val _ = not (null splitths) orelse error "splitto: no given splitths";
-      val sgn = Thm.sign_of_thm genth;
+      val sgn = Thm.theory_of_thm genth;
 
       (* check if we are a member of splitths - FIXME: quicker and
       more flexible with discrim net. *)
       fun solve_by_splitth th split =
           Thm.biresolution false [(false,split)] 1 th;