--- a/src/HOL/Tools/function_package/termination.ML Wed Jun 07 02:01:27 2006 +0200
+++ b/src/HOL/Tools/function_package/termination.ML Wed Jun 07 02:01:28 2006 +0200
@@ -31,7 +31,7 @@
fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _, _) dom =
let
val domT = domain_type (fastype_of f)
- val D = Sign.simple_read_term thy (Type.varifyT (HOLogic.mk_setT domT)) dom
+ val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom
val DT = type_of D
val idomT = HOLogic.dest_setT DT