--- a/src/HOL/Tools/primrec_package.ML Thu Dec 08 20:16:17 2005 +0100
+++ b/src/HOL/Tools/primrec_package.ML Fri Dec 09 09:06:45 2005 +0100
@@ -255,11 +255,11 @@
commas_quote (map fst nameTs1) ^ " ...");
val simps = map (fn (_, t) => standard (Goal.prove thy' [] [] t
(fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))) eqns;
- val (thy'', simps') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
+ val (simps', thy'') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
val thy''' = thy''
- |> (#1 o PureThy.add_thmss [(("simps", simps'),
+ |> (snd o PureThy.add_thmss [(("simps", simps'),
[Simplifier.simp_add_global, RecfunCodegen.add NONE])])
- |> (#1 o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
+ |> (snd o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
|> Theory.parent_path
in
(thy''', simps')