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