diff -r 99577c7085c8 -r 17014b1b9353 src/HOL/Tools/prop_logic.ML
--- a/src/HOL/Tools/prop_logic.ML	Tue Oct 27 17:19:31 2009 +0100
+++ b/src/HOL/Tools/prop_logic.ML	Tue Oct 27 17:34:00 2009 +0100
@@ -37,9 +37,9 @@
 	val eval : (int -> bool) -> prop_formula -> bool  (* semantics *)
 
 	(* propositional representation of HOL terms *)
-	val prop_formula_of_term : Term.term -> int Termtab.table -> prop_formula * int Termtab.table
+	val prop_formula_of_term : term -> int Termtab.table -> prop_formula * int Termtab.table
 	(* HOL term representation of propositional formulae *)
-	val term_of_prop_formula : prop_formula -> Term.term
+	val term_of_prop_formula : prop_formula -> term
 end;
 
 structure PropLogic : PROP_LOGIC =