src/Provers/classical.ML
changeset 42817 7e819eb7dabb
parent 42812 dda4aef7cba4
child 45375 7fe19930dfc9
equal deleted inserted replaced
42816:ba14eafef077 42817:7e819eb7dabb
   292 fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls;
   292 fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls;
   293 fun delete x = delete_tagged_list (joinrules x);
   293 fun delete x = delete_tagged_list (joinrules x);
   294 fun delete' x = delete_tagged_list (joinrules' x);
   294 fun delete' x = delete_tagged_list (joinrules' x);
   295 
   295 
   296 fun string_of_thm NONE = Display.string_of_thm_without_context
   296 fun string_of_thm NONE = Display.string_of_thm_without_context
   297   | string_of_thm (SOME context) =
   297   | string_of_thm (SOME context) = Display.string_of_thm (Context.proof_of context);
   298       Display.string_of_thm (Context.cases Syntax.init_pretty_global I context);
       
   299 
   298 
   300 fun make_elim context th =
   299 fun make_elim context th =
   301   if has_fewer_prems 1 th then
   300   if has_fewer_prems 1 th then
   302     error ("Ill-formed destruction rule\n" ^ string_of_thm context th)
   301     error ("Ill-formed destruction rule\n" ^ string_of_thm context th)
   303   else Tactic.make_elim th;
   302   else Tactic.make_elim th;