tuned;
authorwenzelm
Sat Oct 07 01:30:58 2006 +0200 (2006-10-07)
changeset 20872528054ca23e3
parent 20871 da3a43cdbe8d
child 20873 4066ee15b278
tuned;
src/HOL/Tools/inductive_package.ML
src/HOL/simpdata.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof.ML
src/Pure/old_goals.ML
src/Pure/simplifier.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Oct 06 15:39:29 2006 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Oct 07 01:30:58 2006 +0200
     1.3 @@ -138,7 +138,7 @@
     1.4          | _ => [standard (thm' RS (thm' RS eq_to_mono2))]);
     1.5      val concl = concl_of thm
     1.6    in
     1.7 -    if Logic.is_equals concl then
     1.8 +    if can Logic.dest_equals concl then
     1.9        eq2mono (thm RS meta_eq_to_obj_eq)
    1.10      else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then
    1.11        eq2mono thm
     2.1 --- a/src/HOL/simpdata.ML	Fri Oct 06 15:39:29 2006 +0200
     2.2 +++ b/src/HOL/simpdata.ML	Sat Oct 07 01:30:58 2006 +0200
     2.3 @@ -272,7 +272,7 @@
     2.4    (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
     2.5       rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
     2.6     in mk_meta_eq rl' handle THM _ =>
     2.7 -     if Logic.is_equals (concl_of rl') then rl'
     2.8 +     if can Logic.dest_equals (concl_of rl') then rl'
     2.9       else error "Conclusion of congruence rules must be =-equality"
    2.10     end);
    2.11  
     3.1 --- a/src/Pure/Isar/locale.ML	Fri Oct 06 15:39:29 2006 +0200
     3.2 +++ b/src/Pure/Isar/locale.ML	Sat Oct 07 01:30:58 2006 +0200
     3.3 @@ -898,7 +898,7 @@
     3.4          val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
     3.5          val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
     3.6              let val ((c, _), t') = LocalDefs.cert_def ctxt t
     3.7 -            in (t', ((if name = "" then Thm.def_name c else name, atts), [(t', ps)])) end);
     3.8 +            in (t', ((Thm.def_name_optional c name, atts), [(t', ps)])) end);
     3.9          val (_, ctxt') =
    3.10            ctxt |> fold (Variable.fix_frees o #1) asms
    3.11            |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
    3.12 @@ -1455,13 +1455,10 @@
    3.13  (* print locale *)
    3.14  
    3.15  fun print_locale thy show_facts import body =
    3.16 -  let
    3.17 -    val (all_elems, ctxt) = read_expr import body (ProofContext.init thy);
    3.18 -    val prt_elem = Element.pretty_ctxt ctxt;
    3.19 -  in
    3.20 +  let val (all_elems, ctxt) = read_expr import body (ProofContext.init thy) in
    3.21      Pretty.big_list "locale elements:" (all_elems
    3.22        |> (if show_facts then I else filter (fn Notes _ => false | _ => true))
    3.23 -      |> map (Pretty.chunks o prt_elem))
    3.24 +      |> map (Pretty.chunks o Element.pretty_ctxt ctxt))
    3.25      |> Pretty.writeln
    3.26    end;
    3.27  
     4.1 --- a/src/Pure/Isar/proof.ML	Fri Oct 06 15:39:29 2006 +0200
     4.2 +++ b/src/Pure/Isar/proof.ML	Sat Oct 07 01:30:58 2006 +0200
     4.3 @@ -557,7 +557,7 @@
     4.4      val ((raw_names, raw_atts), (vars, raw_rhss)) =
     4.5        args |> split_list |>> split_list ||> split_list;
     4.6      val xs = map #1 vars;
     4.7 -    val names = map (fn ("", x) => Thm.def_name x | (name, _) => name) (raw_names ~~ xs);
     4.8 +    val names = map2 Thm.def_name_optional xs raw_names;
     4.9      val atts = map (map (prep_att thy)) raw_atts;
    4.10      val (rhss, state') = state |> map_context_result (prep_binds false (map swap raw_rhss));
    4.11      val eqs = LocalDefs.mk_def (context_of state') (xs ~~ rhss);
     5.1 --- a/src/Pure/old_goals.ML	Fri Oct 06 15:39:29 2006 +0200
     5.2 +++ b/src/Pure/old_goals.ML	Sat Oct 07 01:30:58 2006 +0200
     5.3 @@ -156,7 +156,7 @@
     5.4        val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
     5.5        val (As, B) = Logic.strip_horn horn;
     5.6        val atoms = atomic andalso
     5.7 -            forall (fn t => not(Logic.is_implies t orelse Logic.is_all t)) As;
     5.8 +            forall (fn t => not (can Logic.dest_implies t orelse Logic.is_all t)) As;
     5.9        val (As,B) = if atoms then ([],horn) else (As,B);
    5.10        val cAs = map (cterm_of thy) As;
    5.11        val prems = map (rewrite_rule rths o forall_elim_vars 0 o Thm.assume) cAs;
     6.1 --- a/src/Pure/simplifier.ML	Fri Oct 06 15:39:29 2006 +0200
     6.2 +++ b/src/Pure/simplifier.ML	Sat Oct 07 01:30:58 2006 +0200
     6.3 @@ -335,7 +335,7 @@
     6.4      val safe_solver = mk_solver "easy safe" safe_solver_tac;
     6.5  
     6.6      fun mk_eq thm =
     6.7 -      if Logic.is_equals (Thm.concl_of thm) then [thm]
     6.8 +      if can Logic.dest_equals (Thm.concl_of thm) then [thm]
     6.9        else [thm RS reflect] handle THM _ => [];
    6.10  
    6.11      fun mksimps thm = mk_eq (Drule.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);