--- a/src/HOL/Statespace/DistinctTreeProver.thy Wed Oct 24 19:21:39 2007 +0200
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Wed Oct 24 19:21:40 2007 +0200
@@ -7,7 +7,7 @@
theory DistinctTreeProver
imports Main
-uses (distinct_tree_prover)
+uses ("distinct_tree_prover.ML")
begin
text {* A state space manages a set of (abstract) names and assumes
@@ -632,7 +632,7 @@
text {* Now we have all the theorems in place that are needed for the
certificate generating ML functions. *}
-use distinct_tree_prover
+use "distinct_tree_prover.ML"
(* Uncomment for profiling or debugging *)
(*