--- a/src/HOL/Tools/BNF/bnf_axiomatization.ML Sat May 28 17:35:12 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_axiomatization.ML Sat May 28 21:38:58 2016 +0200
@@ -81,8 +81,10 @@
val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
- val (((_, [raw_thms])), lthy) = Local_Theory.background_theory_result
- (Specification.axiomatization [] [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy;
+ val (((_, raw_thms)), lthy) = Local_Theory.background_theory_result
+ (Specification.axiomatization [] [] []
+ (map_index (fn (i, ax) =>
+ ((mk_b ("axiom" ^ string_of_int (i + 1)) Binding.empty, []), ax)) (flat all_goalss))) lthy;
fun mk_wit_thms set_maps =
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)