src/HOL/Tools/inductive_realizer.ML
changeset 37136 e0c9d3e49e15
parent 36945 9bec62c10714
child 37236 739d8b9c59da
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed May 26 16:05:25 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed May 26 16:05:25 2010 +0200
     1.3 @@ -389,7 +389,7 @@
     1.4            end) (rlzs ~~ rnames);
     1.5          val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
     1.6            (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
     1.7 -        val rews = map mk_meta_eq (fst_conv :: snd_conv :: rec_thms);
     1.8 +        val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms);
     1.9          val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
    1.10            [rtac (#raw_induct ind_info) 1,
    1.11             rewrite_goals_tac rews,