1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Nov 04 16:53:43 2013 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Nov 04 17:25:36 2013 +0100
     1.3 @@ -280,7 +280,7 @@
     1.4              |> map (fn (resultt, (_, prems)) =>
     1.5                Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt]))))
     1.6            end
     1.7 -      val intr_ts = maps mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))
     1.8 +      val intr_tss = map mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))
     1.9        val (intrs, thy') = thy
    1.10          |> Sign.add_consts_i
    1.11            (map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn))
    1.12 @@ -288,7 +288,7 @@
    1.13          |> fold_map Specification.axiom
    1.14              (map_index (fn (j, (predname, t)) =>
    1.15                  ((Binding.name (Long_Name.base_name predname ^ "_intro_" ^ string_of_int (j + 1)), []), t))
    1.16 -              (prednames ~~ intr_ts))
    1.17 +              (maps (uncurry (map o pair)) (prednames ~~ intr_tss)))
    1.18        val specs = map (fn predname => (predname,
    1.19            map Drule.export_without_context (filter (Predicate_Compile_Aux.is_intro predname) intrs)))
    1.20          dst_prednames