src/Pure/term.ML
changeset 20129 95e84d2c9f2c
parent 20122 27255556b762
child 20148 8a5fa86994c7
     1.1 --- a/src/Pure/term.ML	Fri Jul 14 14:19:48 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Fri Jul 14 14:37:15 2006 +0200
     1.3 @@ -172,7 +172,7 @@
     1.4    val term_ord: term * term -> order
     1.5    val hd_ord: term * term -> order
     1.6    val termless: term * term -> bool
     1.7 -  val term_lpo: (string -> int) -> term * term -> order
     1.8 +  val term_lpo: (term -> int) -> term * term -> order
     1.9    val match_bvars: (term * term) * (string * string) list -> (string * string) list
    1.10    val rename_abs: term -> term -> term -> term option
    1.11    val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
    1.12 @@ -646,23 +646,26 @@
    1.13    Without variables.  Const, Var, Bound, Free and Abs are treated all as
    1.14    constants.
    1.15  
    1.16 -  f_ord maps strings to integers and serves two purposes:
    1.17 +  f_ord maps terms to integers and serves two purposes:
    1.18    - Predicate on constant symbols.  Those that are not recognised by f_ord
    1.19      must be mapped to ~1.
    1.20    - Order on the recognised symbols.  These must be mapped to distinct
    1.21      integers >= 0.
    1.22 -
    1.23 +  The argument of f_ord is never an application.
    1.24  *)
    1.25  
    1.26  local
    1.27 -fun dest_hd f_ord (Const (a, T)) =
    1.28 -      let val ord = f_ord a in
    1.29 -        if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0)
    1.30 +
    1.31 +fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0)
    1.32 +  | unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0)
    1.33 +  | unrecognized (Var v) = ((1, v), 1)
    1.34 +  | unrecognized (Bound i) = ((1, (("", i), dummyT)), 2)
    1.35 +  | unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
    1.36 +
    1.37 +fun dest_hd f_ord t =
    1.38 +      let val ord = f_ord t in
    1.39 +        if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0)
    1.40        end
    1.41 -  | dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0)
    1.42 -  | dest_hd _ (Var v) = ((1, v), 1)
    1.43 -  | dest_hd _ (Bound i) = ((1, (("", i), dummyT)), 2)
    1.44 -  | dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
    1.45  
    1.46  fun term_lpo f_ord (s, t) =
    1.47    let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in