src/Pure/goals.ML
changeset 11963 a6608d44a46b
parent 11884 341b1fbc6130
child 12012 1d534baa2827
equal deleted inserted replaced
11962:4c6585866fb2 11963:a6608d44a46b
   210       val (_,As,B) = Logic.strip_horn(horn);
   210       val (_,As,B) = Logic.strip_horn(horn);
   211       val atoms = atomic andalso
   211       val atoms = atomic andalso
   212             forall (fn t => not(Logic.is_implies t orelse Logic.is_all t)) As;
   212             forall (fn t => not(Logic.is_implies t orelse Logic.is_all t)) As;
   213       val (As,B) = if atoms then ([],horn) else (As,B);
   213       val (As,B) = if atoms then ([],horn) else (As,B);
   214       val cAs = map (cterm_of sign) As;
   214       val cAs = map (cterm_of sign) As;
   215       val prems = map (rewrite_rule rths o forall_elim_vars(0) o assume) cAs;
   215       val prems = map (rewrite_rule rths o forall_elim_vars 0 o Thm.assume) cAs;
   216       val cB = cterm_of sign B;
   216       val cB = cterm_of sign B;
   217       val st0 = let val st = Drule.mk_triv_goal cB
   217       val st0 = let val st = Drule.impose_hyps cAs (Drule.mk_triv_goal cB)
   218                 in  rewrite_goals_rule rths st end
   218                 in  rewrite_goals_rule rths st end
   219       (*discharges assumptions from state in the order they appear in goal;
   219       (*discharges assumptions from state in the order they appear in goal;
   220 	checks (if requested) that resulting theorem is equivalent to goal. *)
   220 	checks (if requested) that resulting theorem is equivalent to goal. *)
   221       fun mkresult (check,state) =
   221       fun mkresult (check,state) =
   222         let val state = Seq.hd (flexflex_rule state)
   222         let val state = Seq.hd (flexflex_rule state)