changeset 26336 | a0e2b706ce73 |
parent 25999 | f8bcd311d501 |
child 26343 | 0dd2eab7b296 |
--- a/src/HOL/Statespace/state_space.ML Wed Mar 19 18:15:25 2008 +0100 +++ b/src/HOL/Statespace/state_space.ML Wed Mar 19 22:27:57 2008 +0100 @@ -270,7 +270,7 @@ fun solve_tac ctxt (_,i) st = let - val distinct_thm = ProofContext.get_thm ctxt (Name dist_thm_name); + val distinct_thm = ProofContext.get_thm ctxt (Facts.Named (dist_thm_name, NONE)); val goal = List.nth (cprems_of st,i-1); val rule = DistinctTreeProver.distinct_implProver distinct_thm goal; in EVERY [rtac rule i] st