src/Tools/misc_legacy.ML
changeset 52223 5bb6ae8acb87
parent 51429 48eb29821bd9
child 56147 9589605bcf41
equal deleted inserted replaced
52222:0fa3b456a267 52223:5bb6ae8acb87
   201                 (*discharge assumptions from state in same order*)
   201                 (*discharge assumptions from state in same order*)
   202                 (implies_intr_list emBs
   202                 (implies_intr_list emBs
   203                   (forall_intr_list cparams (implies_intr_list chyps Cth)))
   203                   (forall_intr_list cparams (implies_intr_list chyps Cth)))
   204         end
   204         end
   205       (*function to replace the current subgoal*)
   205       (*function to replace the current subgoal*)
   206       fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
   206       fun next st =
       
   207         Thm.bicompose {flatten = true, match = false, incremented = false}
       
   208           (false, relift st, nprems_of st) gno state
   207   in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
   209   in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
   208 
   210 
   209 fun print_vars_terms n thm =
   211 fun print_vars_terms n thm =
   210   let
   212   let
   211     val thy = theory_of_thm thm
   213     val thy = theory_of_thm thm