--- a/src/Pure/more_thm.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/more_thm.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/more_thm.ML
- ID: $Id$
Author: Makarius
Further operations on type ctyp/cterm/thm, outside the inference kernel.
@@ -128,12 +127,12 @@
val {shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = Thm.rep_thm th1;
val {shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = Thm.rep_thm th2;
in
- (case Term.fast_term_ord (prop1, prop2) of
+ (case TermOrd.fast_term_ord (prop1, prop2) of
EQUAL =>
- (case list_ord (prod_ord Term.fast_term_ord Term.fast_term_ord) (tpairs1, tpairs2) of
+ (case list_ord (prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord) (tpairs1, tpairs2) of
EQUAL =>
- (case list_ord Term.fast_term_ord (hyps1, hyps2) of
- EQUAL => list_ord Term.sort_ord (shyps1, shyps2)
+ (case list_ord TermOrd.fast_term_ord (hyps1, hyps2) of
+ EQUAL => list_ord TermOrd.sort_ord (shyps1, shyps2)
| ord => ord)
| ord => ord)
| ord => ord)