src/HOL/Import/proof_kernel.ML
changeset 29289 f45c9c3b40a3
parent 29281 b22ccb3998db
child 29585 c23295521af5
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Jan 01 14:23:39 2009 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Jan 01 14:23:39 2009 +0100
     1.3 @@ -280,14 +280,12 @@
     1.4            | itr (a::rst) = i=a orelse itr rst
     1.5      in itr L end;
     1.6  
     1.7 -fun insert i L = if i mem L then L else i::L
     1.8 -
     1.9  fun mk_set [] = []
    1.10 -  | mk_set (a::rst) = insert a (mk_set rst)
    1.11 +  | mk_set (a::rst) = insert (op =) a (mk_set rst)
    1.12  
    1.13  fun [] union S = S
    1.14    | S union [] = S
    1.15 -  | (a::rst) union S2 = rst union (insert a S2)
    1.16 +  | (a::rst) union S2 = rst union (insert (op =) a S2)
    1.17  
    1.18  fun implode_subst [] = []
    1.19    | implode_subst (x::r::rest) = ((x,r)::(implode_subst rest))
    1.20 @@ -1213,24 +1211,23 @@
    1.21                | NONE => NONE
    1.22          end
    1.23  
    1.24 -fun non_trivial_term_consts tm =
    1.25 -    List.filter (fn c => not (c = "Trueprop" orelse
    1.26 -                         c = "All" orelse
    1.27 -                         c = "op -->" orelse
    1.28 -                         c = "op &" orelse
    1.29 -                         c = "op =")) (OldTerm.term_consts tm)
    1.30 +fun non_trivial_term_consts t = fold_aterms
    1.31 +  (fn Const (c, _) =>
    1.32 +      if c = "Trueprop" orelse c = "All" orelse c = "op -->" orelse c = "op &" orelse c = "op ="
    1.33 +      then I else insert (op =) c
    1.34 +    | _ => I) t [];
    1.35  
    1.36  fun match_consts t (* th *) =
    1.37      let
    1.38          fun add_consts (Const (c, _), cs) =
    1.39              (case c of
    1.40 -                 "op =" => Library.insert (op =) "==" cs
    1.41 -               | "op -->" => Library.insert (op =) "==>" cs
    1.42 +                 "op =" => insert (op =) "==" cs
    1.43 +               | "op -->" => insert (op =) "==>" cs
    1.44                 | "All" => cs
    1.45                 | "all" => cs
    1.46                 | "op &" => cs
    1.47                 | "Trueprop" => cs
    1.48 -               | _ => Library.insert (op =) c cs)
    1.49 +               | _ => insert (op =) c cs)
    1.50            | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
    1.51            | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
    1.52            | add_consts (_, cs) = cs
    1.53 @@ -1297,7 +1294,7 @@
    1.54              let
    1.55                  val _ = (message "Looking for conclusion:";
    1.56                           if_debug prin isaconc)
    1.57 -                val cs = non_trivial_term_consts isaconc
    1.58 +                val cs = non_trivial_term_consts isaconc;
    1.59                  val _ = (message "Looking for consts:";
    1.60                           message (commas cs))
    1.61                  val pot_thms = Shuffler.find_potential thy isaconc