src/Pure/Isar/calculation.ML
changeset 7475 dc4f8d6ee0d2
parent 7414 9bc7797d1249
child 7554 30327f9f6b4a
equal deleted inserted replaced
7474:43cedde6d52a 7475:dc4f8d6ee0d2
   123   let
   123   let
   124     fun err_if b msg = if b then raise Proof.STATE (msg, state) else ();
   124     fun err_if b msg = if b then raise Proof.STATE (msg, state) else ();
   125     val facts = Proof.the_facts state;
   125     val facts = Proof.the_facts state;
   126     val rules = Seq.of_list (if_none opt_rules [] @ get_local_rules state);
   126     val rules = Seq.of_list (if_none opt_rules [] @ get_local_rules state);
   127 
   127 
   128     fun differ thms thms' =
   128     fun differ thms thms' = not (Library.equal_lists Thm.eq_thm (thms, thms'));
   129       length thms <> length thms' orelse exists2 (not o Thm.eq_thm) (thms, thms');
       
   130     fun combine thms =
   129     fun combine thms =
   131       Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve (thms @ facts)) rules));
   130       Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve (thms @ facts)) rules));
   132 
   131 
   133     val (initial, calculations) =
   132     val (initial, calculations) =
   134       (case get_calculation state of
   133       (case get_calculation state of