tuned;
authorwenzelm
Wed Nov 09 16:26:54 2005 +0100 (2005-11-09)
changeset 18139b15981aedb7b
parent 18138 04f0e4ca1451
child 18140 691c64d615a5
tuned;
TFL/post.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/goal.ML
src/Pure/theory.ML
     1.1 --- a/TFL/post.ML	Wed Nov 09 16:26:53 2005 +0100
     1.2 +++ b/TFL/post.ML	Wed Nov 09 16:26:54 2005 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4   *--------------------------------------------------------------------------*)
     1.5  fun termination_goals rules =
     1.6      map (Type.freeze o HOLogic.dest_Trueprop)
     1.7 -      (foldr (fn (th,A) => union_term (prems_of th, A)) [] rules);
     1.8 +      (foldr (fn (th,A) => gen_union (op aconv) (prems_of th, A)) [] rules);
     1.9  
    1.10  (*---------------------------------------------------------------------------
    1.11   * Finds the termination conditions in (highly massaged) definition and
     2.1 --- a/src/Pure/Syntax/printer.ML	Wed Nov 09 16:26:53 2005 +0100
     2.2 +++ b/src/Pure/Syntax/printer.ML	Wed Nov 09 16:26:54 2005 +0100
     2.3 @@ -111,7 +111,7 @@
     2.4  (** term_to_ast **)
     2.5  
     2.6  fun mark_freevars ((t as Const (c, _)) $ u) =
     2.7 -      if c mem_string SynExt.standard_token_markers then (t $ u)
     2.8 +      if member (op =) SynExt.standard_token_markers c then (t $ u)
     2.9        else t $ mark_freevars u
    2.10    | mark_freevars (t $ u) = mark_freevars t $ mark_freevars u
    2.11    | mark_freevars (Abs (x, T, t)) = Abs (x, T, mark_freevars t)
    2.12 @@ -126,11 +126,11 @@
    2.13      fun prune_typs (t_seen as (Const _, _)) = t_seen
    2.14        | prune_typs (t as Free (x, ty), seen) =
    2.15            if ty = dummyT then (t, seen)
    2.16 -          else if no_freeTs orelse t mem seen then (Lexicon.free x, seen)
    2.17 +          else if no_freeTs orelse member (op aconv) seen t then (Lexicon.free x, seen)
    2.18            else (t, t :: seen)
    2.19        | prune_typs (t as Var (xi, ty), seen) =
    2.20            if ty = dummyT then (t, seen)
    2.21 -          else if no_freeTs orelse t mem seen then (Lexicon.var xi, seen)
    2.22 +          else if no_freeTs orelse member (op aconv) seen t then (Lexicon.var xi, seen)
    2.23            else (t, t :: seen)
    2.24        | prune_typs (t_seen as (Bound _, _)) = t_seen
    2.25        | prune_typs (Abs (x, ty, t), seen) =
     3.1 --- a/src/Pure/Syntax/syn_trans.ML	Wed Nov 09 16:26:53 2005 +0100
     3.2 +++ b/src/Pure/Syntax/syn_trans.ML	Wed Nov 09 16:26:54 2005 +0100
     3.3 @@ -395,10 +395,10 @@
     3.4  fun antiquote_tr' name =
     3.5    let
     3.6      fun tr' i (t $ u) =
     3.7 -      if u = Bound i then Lexicon.const name $ tr' i t
     3.8 +      if u aconv Bound i then Lexicon.const name $ tr' i t
     3.9        else tr' i t $ tr' i u
    3.10        | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)
    3.11 -      | tr' i a = if a = Bound i then raise Match else a;
    3.12 +      | tr' i a = if a aconv Bound i then raise Match else a;
    3.13    in tr' 0 end;
    3.14  
    3.15  fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t)
     4.1 --- a/src/Pure/goal.ML	Wed Nov 09 16:26:53 2005 +0100
     4.2 +++ b/src/Pure/goal.ML	Wed Nov 09 16:26:54 2005 +0100
     4.3 @@ -2,7 +2,7 @@
     4.4      ID:         $Id$
     4.5      Author:     Makarius and Lawrence C Paulson
     4.6  
     4.7 -Tactical goal state.
     4.8 +Goals in tactical theorem proving.
     4.9  *)
    4.10  
    4.11  signature BASIC_GOAL =
    4.12 @@ -21,9 +21,9 @@
    4.13    val compose_hhf: thm -> int -> thm -> thm Seq.seq
    4.14    val compose_hhf_tac: thm -> int -> tactic
    4.15    val comp_hhf: thm -> thm -> thm
    4.16 -  val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    4.17    val prove_multi: theory -> string list -> term list -> term list ->
    4.18      (thm list -> tactic) -> thm list
    4.19 +  val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    4.20    val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm
    4.21  end;
    4.22  
    4.23 @@ -104,9 +104,9 @@
    4.24    let
    4.25      val prop = Logic.mk_conjunction_list props;
    4.26      val statement = Logic.list_implies (asms, prop);
    4.27 -    val frees = map Term.dest_Free (Term.term_frees statement);
    4.28 +    val frees = Term.add_frees statement [];
    4.29      val fixed_frees = filter_out (member (op =) xs o #1) frees;
    4.30 -    val fixed_tfrees = foldr Term.add_typ_tfrees [] (map #2 fixed_frees);
    4.31 +    val fixed_tfrees = fold (Term.add_tfreesT o #2) fixed_frees [];
    4.32      val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
    4.33  
    4.34      fun err msg = raise ERROR_MESSAGE
    4.35 @@ -136,8 +136,8 @@
    4.36        (Drule.implies_intr_list casms
    4.37          #> Drule.forall_intr_list cparams
    4.38          #> norm_hhf
    4.39 -        #> (#1 o Thm.varifyT' fixed_tfrees)
    4.40 -        #> Drule.zero_var_indexes)
    4.41 +        #> Thm.varifyT' fixed_tfrees
    4.42 +        #-> K Drule.zero_var_indexes)
    4.43    end;
    4.44  
    4.45  
     5.1 --- a/src/Pure/theory.ML	Wed Nov 09 16:26:53 2005 +0100
     5.2 +++ b/src/Pure/theory.ML	Wed Nov 09 16:26:54 2005 +0100
     5.3 @@ -273,8 +273,8 @@
     5.4      val show_tfrees = commas_quote o map fst;
     5.5  
     5.6      val lhs_nofrees = filter (not o can dest_free) args;
     5.7 -    val lhs_dups = duplicates args;
     5.8 -    val rhs_extras = term_frees rhs |> fold (remove op =) args;
     5.9 +    val lhs_dups = gen_duplicates (op aconv) args;
    5.10 +    val rhs_extras = term_frees rhs |> fold (remove op aconv) args;
    5.11      val rhs_extrasT = term_tfrees rhs |> fold (remove op =) (typ_tfrees T);
    5.12    in
    5.13      if not (null lhs_nofrees) then