cosmetics
authorblanchet
Fri Aug 27 13:19:48 2010 +0200 (2010-08-27)
changeset 38824f74513bbe627
parent 38823 828e68441a2f
child 38825 4ec3cbd95f25
cosmetics
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 27 13:12:23 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Aug 27 13:19:48 2010 +0200
     1.3 @@ -74,13 +74,14 @@
     1.4  and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")"
     1.5  
     1.6  (*Is the second type an instance of the first one?*)
     1.7 -fun match_pattern (PApp (a, T), PApp (b, U)) =
     1.8 -    a = b andalso match_patterns (T, U)
     1.9 -  | match_pattern (PVar, _) = true
    1.10 -  | match_pattern (_, PVar) = false
    1.11 -and match_patterns ([], []) = true
    1.12 -  | match_patterns (T :: Ts, U :: Us) =
    1.13 -    match_pattern (T, U) andalso match_patterns (Ts, Us)
    1.14 +fun match_pattern (PVar, _) = true
    1.15 +  | match_pattern (PApp _, PVar) = false
    1.16 +  | match_pattern (PApp (s, ps), PApp (t, qs)) =
    1.17 +    s = t andalso match_patterns (ps, qs)
    1.18 +and match_patterns (_, []) = true
    1.19 +  | match_patterns ([], _) = false
    1.20 +  | match_patterns (p :: ps, q :: qs) =
    1.21 +    match_pattern (p, q) andalso match_patterns (ps, qs)
    1.22  
    1.23  (* Is there a unifiable constant? *)
    1.24  fun pconst_mem f const_tab (s, ps) =
    1.25 @@ -108,12 +109,12 @@
    1.26  
    1.27  (* Add a pconstant to the table, but a [] entry means a standard
    1.28     connective, which we ignore.*)
    1.29 -fun add_pconst_to_table also_skolem (c, Ts) =
    1.30 +fun add_pconst_to_table also_skolem (c, ps) =
    1.31    if member (op =) boring_consts c orelse
    1.32       (not also_skolem andalso String.isPrefix skolem_prefix c) then
    1.33      I
    1.34    else
    1.35 -    Symtab.map_default (c, [Ts]) (fn Tss => insert (op =) Ts Tss)
    1.36 +    Symtab.map_default (c, [ps]) (insert (op =) ps)
    1.37  
    1.38  fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
    1.39  
    1.40 @@ -223,8 +224,8 @@
    1.41  (**** Actual Filtering Code ****)
    1.42  
    1.43  (*The frequency of a constant is the sum of those of all instances of its type.*)
    1.44 -fun pconst_freq match const_tab (c, Ts) =
    1.45 -  CTtab.fold (fn (Ts', m) => match (Ts, Ts') ? Integer.add m)
    1.46 +fun pconst_freq match const_tab (c, ps) =
    1.47 +  CTtab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
    1.48               (the (Symtab.lookup const_tab c)) 0
    1.49  
    1.50