src/HOL/Statespace/distinct_tree_prover.ML
changeset 26343 0dd2eab7b296
parent 26336 a0e2b706ce73
child 29064 70a61d58460e
     1.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Wed Mar 19 22:50:42 2008 +0100
     1.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Thu Mar 20 00:20:44 2008 +0100
     1.3 @@ -339,7 +339,7 @@
     1.4  
     1.5  fun neq_x_y ctxt x y name =
     1.6    (let
     1.7 -    val dist_thm = the (try (ProofContext.get_thm ctxt) (Facts.Named (name, NONE)));
     1.8 +    val dist_thm = the (try (ProofContext.get_thm ctxt) name);
     1.9      val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
    1.10      val tree = term_of ctree;
    1.11      val x_path = the (find_tree x tree);