src/HOL/Statespace/distinct_tree_prover.ML

--- a/src/HOL/Statespace/distinct_tree_prover.ML	Wed Mar 19 22:50:42 2008 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Thu Mar 20 00:20:44 2008 +0100
@@ -339,7 +339,7 @@
 
 fun neq_x_y ctxt x y name =
   (let
-    val dist_thm = the (try (ProofContext.get_thm ctxt) (Facts.Named (name, NONE)));
+    val dist_thm = the (try (ProofContext.get_thm ctxt) name);
     val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
     val tree = term_of ctree;
     val x_path = the (find_tree x tree);