src/HOL/Statespace/distinct_tree_prover.ML
changeset 26336 a0e2b706ce73
parent 25408 156f6f7082b8
child 26343 0dd2eab7b296
     1.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Wed Mar 19 18:15:25 2008 +0100
     1.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Wed Mar 19 22:27:57 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) (PureThy.Name name)); 
     1.8 +    val dist_thm = the (try (ProofContext.get_thm ctxt) (Facts.Named (name, NONE)));
     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);