distinct (op =);
authorwenzelm
Tue Feb 21 15:06:50 2006 +0100 (2006-02-21)
changeset 19115bc8da9b4a81c
parent 19114 dfe6ace301c3
child 19116 d065ec558092
distinct (op =);
removed spurious PolyML.print;
src/HOL/Nominal/nominal_induct.ML
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Mon Feb 20 21:51:50 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Tue Feb 21 15:06:50 2006 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4          List.mapPartial (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst)
     1.5        end;
     1.6       val substs =
     1.7 -       map2 subst insts rules |> List.concat |> distinct
     1.8 +       map2 subst insts rules |> List.concat |> distinct (op =)
     1.9         |> map (pairself (Thm.cterm_of thy));
    1.10    in (((cases, concls), consumes), Drule.cterm_instantiate substs rule) end;
    1.11  
    1.12 @@ -90,9 +90,9 @@
    1.13      val ((insts, defs), defs_ctxt) = fold_map InductMethod.add_defs def_insts ctxt |>> split_list;
    1.14      val atomized_defs = map (map ObjectLogic.atomize_thm) defs;
    1.15  
    1.16 -    val finish_rule = PolyML.print #>
    1.17 +    val finish_rule =
    1.18        split_all_tuples
    1.19 -      #> rename_params_rule true (map (ProofContext.revert_skolem defs_ctxt o fst) avoiding) #> PolyML.print;
    1.20 +      #> rename_params_rule true (map (ProofContext.revert_skolem defs_ctxt o fst) avoiding);
    1.21      fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (InductMethod.rulified_term r);
    1.22    in
    1.23      (fn i => fn st =>
    1.24 @@ -108,9 +108,10 @@
    1.25                  (nth_list fixings (j - 1))))
    1.26            THEN' InductMethod.inner_atomize_tac) j))
    1.27          THEN' InductMethod.atomize_tac) i st |> Seq.maps (fn st' =>
    1.28 -            InductMethod.guess_instance (finish_rule (InductMethod.internalize more_consumes rule)) i (PolyML.print st')
    1.29 +            InductMethod.guess_instance
    1.30 +              (finish_rule (InductMethod.internalize more_consumes rule)) i st'
    1.31              |> Seq.maps (fn rule' =>
    1.32 -              CASES (rule_cases (PolyML.print rule') cases)
    1.33 +              CASES (rule_cases rule' cases)
    1.34                  (Tactic.rtac (rename_params_rule false [] rule') i THEN
    1.35                    PRIMSEQ (ProofContext.exports defs_ctxt ctxt)) st'))))
    1.36      THEN_ALL_NEW_CASES InductMethod.rulify_tac