--- a/src/HOL/Tools/Qelim/langford.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/Qelim/langford.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,3 +1,7 @@
+(* Title: HOL/Tools/Qelim/langford.ML
+ Author: Amine Chaieb, TU Muenchen
+*)
+
signature LANGFORD_QE =
sig
val dlo_tac : Proof.context -> int -> tactic
@@ -211,7 +215,7 @@
let
fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
- val ts = sort (fn (a,b) => Term.fast_term_ord (term_of a, term_of b)) (f p)
+ val ts = sort (fn (a,b) => TermOrd.fast_term_ord (term_of a, term_of b)) (f p)
val p' = fold_rev gen ts p
in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));