equal
deleted
inserted
replaced
173 |
173 |
174 val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info) |
174 val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info) |
175 val eqn_thms = |
175 val eqn_thms = |
176 eqn_terms |> map (fn t => |
176 eqn_terms |> map (fn t => |
177 Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t) |
177 Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t) |
178 (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])); |
178 (fn _ => EVERY [rewrite_goals_tac rewrites, rtac @{thm refl} 1])); |
179 |
179 |
180 val (eqn_thms', thy2) = |
180 val (eqn_thms', thy2) = |
181 thy1 |
181 thy1 |
182 |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts); |
182 |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts); |
183 val (_, thy3) = |
183 val (_, thy3) = |