--- 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 =