src/HOL/Tools/inductive_realizer.ML
changeset 33955 fff6f11b1f09
parent 33726 0878aecbf119
child 33957 e9afca2118d4
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -67,7 +67,7 @@
     1.4      val Tvs = map TVar iTs;
     1.5      val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
     1.6        (Logic.strip_imp_concl (prop_of (hd intrs))));
     1.7 -    val params = map dest_Var (Library.take (nparms, ts));
     1.8 +    val params = map dest_Var ((uncurry take) (nparms, ts));
     1.9      val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs));
    1.10      fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),
    1.11        map (Logic.unvarifyT o snd) (subtract (op =) params (rev (Term.add_vars (prop_of intr) []))) @