src/Pure/Isar/calculation.ML
changeset 7197 3ddf4a55d765
parent 6903 682f8a9ec75d
child 7414 9bc7797d1249
equal deleted inserted replaced
7196:c8d1002060e8 7197:3ddf4a55d765
   120 
   120 
   121 fun calculate final opt_rules print state =
   121 fun calculate final opt_rules print state =
   122   let
   122   let
   123     fun err_if b msg = if b then raise Proof.STATE (msg, state) else ();
   123     fun err_if b msg = if b then raise Proof.STATE (msg, state) else ();
   124     val fact = Proof.the_fact state;
   124     val fact = Proof.the_fact state;
   125     val rules = Seq.of_list (case opt_rules of None => get_local_rules state | Some thms => thms);
   125     val rules = Seq.of_list (if_none opt_rules [] @ get_local_rules state);
   126     val (initial, calculations) =
   126     val (initial, calculations) =
   127       (case get_calculation state of
   127       (case get_calculation state of
   128         None => (true, Seq.single fact)
   128         None => (true, Seq.single fact)
   129       | Some thm => (false, Seq.flat (Seq.map (Method.multi_resolve [thm, fact]) rules)));
   129       | Some thm => (false, Seq.flat (Seq.map (Method.multi_resolve [thm, fact]) rules)));
   130   in
   130   in