--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Dec 12 20:55:57 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Dec 12 23:05:21 2011 +0100
@@ -76,11 +76,11 @@
| _ => NONE) cos;
fun prep_inject (trueprop $ (equiv $ (_ $ t1 $ t2) $ rhs)) =
trueprop $ (equiv $ mk_eq (t1, t2) $ rhs);
- val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr] vs) index);
+ val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr]) index);
fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) =
[trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
val distincts =
- maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
+ maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr]) index));
val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
val simpset =
Simplifier.global_context thy