src/Pure/thm.ML
 changeset 29269 5c25a2012975 parent 29003 d8d3cbbb6fcc child 29272 fb3ccf499df5
```     1.1 --- a/src/Pure/thm.ML	Wed Dec 31 00:08:14 2008 +0100
1.2 +++ b/src/Pure/thm.ML	Wed Dec 31 15:30:10 2008 +0100
1.3 @@ -1,7 +1,6 @@
1.4  (*  Title:      Pure/thm.ML
1.5 -    ID:         \$Id\$
1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 -    Copyright   1994  University of Cambridge
1.8 +    Author:     Makarius
1.9
1.10  The very core of Isabelle's Meta Logic: certified types and terms,
1.11  derivations, theorems, framework rules (including lifting and
1.12 @@ -380,9 +379,9 @@
1.13
1.14  fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop;
1.15
1.16 -val union_hyps = OrdList.union Term.fast_term_ord;
1.17 -val insert_hyps = OrdList.insert Term.fast_term_ord;
1.18 -val remove_hyps = OrdList.remove Term.fast_term_ord;
1.19 +val union_hyps = OrdList.union TermOrd.fast_term_ord;
1.20 +val insert_hyps = OrdList.insert TermOrd.fast_term_ord;
1.21 +val remove_hyps = OrdList.remove TermOrd.fast_term_ord;
1.22
1.23
1.24  (* merge theories of cterms/thms -- trivial absorption only *)
1.25 @@ -1561,9 +1560,9 @@
1.26  (*Quick test whether rule is resolvable with the subgoal with hyps Hs
1.27    and conclusion B.  If eres_flg then checks 1st premise of rule also*)
1.28  fun could_bires (Hs, B, eres_flg, rule) =
1.29 -    let fun could_reshyp (A1::_) = exists (fn H => could_unify (A1, H)) Hs
1.30 +    let fun could_reshyp (A1::_) = exists (fn H => Term.could_unify (A1, H)) Hs
1.31            | could_reshyp [] = false;  (*no premise -- illegal*)
1.32 -    in  could_unify(concl_of rule, B) andalso
1.33 +    in  Term.could_unify(concl_of rule, B) andalso
1.34          (not eres_flg  orelse  could_reshyp (prems_of rule))
1.35      end;
1.36
```