src/HOL/Nominal/nominal_induct.ML
changeset 32952 aeb1e44fbc19
parent 30549 d2d7874648bd
child 33368 b1cf34f1855c
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Thu Oct 15 23:10:35 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Thu Oct 15 23:28:10 2009 +0200
     1.3 @@ -50,10 +50,10 @@
     1.4        in
     1.5          (P, tuple_fun (map #2 avoiding) (Term.dest_Var P)) ::
     1.6          (x, tuple (map Free avoiding)) ::
     1.7 -        List.mapPartial (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst)
     1.8 +        map_filter (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst)
     1.9        end;
    1.10       val substs =
    1.11 -       map2 subst insts concls |> List.concat |> distinct (op =)
    1.12 +       map2 subst insts concls |> flat |> distinct (op =)
    1.13         |> map (pairself (Thm.cterm_of (ProofContext.theory_of ctxt)));
    1.14    in 
    1.15      (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) 
    1.16 @@ -98,7 +98,7 @@
    1.17      (fn i => fn st =>
    1.18        rules
    1.19        |> inst_mutual_rule ctxt insts avoiding
    1.20 -      |> RuleCases.consume (List.concat defs) facts
    1.21 +      |> RuleCases.consume (flat defs) facts
    1.22        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
    1.23          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
    1.24            (CONJUNCTS (ALLGOALS