src/HOL/Nominal/nominal_inductive.ML
changeset 44045 2814ff2a6e3e
parent 43326 47cf4bc789aa
child 44689 f247fc952f31
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sun Jul 31 11:13:38 2011 -0700
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Aug 01 12:08:53 2011 +0200
     1.3 @@ -158,7 +158,7 @@
     1.4          [] => ()
     1.5        | xs => error ("Missing equivariance theorem for predicate(s): " ^
     1.6            commas_quote xs));
     1.7 -    val induct_cases = map fst (fst (Rule_Cases.get (the
     1.8 +    val induct_cases = map (fst o fst) (fst (Rule_Cases.get (the
     1.9        (Induct.lookup_inductP ctxt (hd names)))));
    1.10      val ([raw_induct'], ctxt') = Variable.import_terms false [prop_of raw_induct] ctxt;
    1.11      val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>