Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Statespace/state_fun.ML
changeset 38012 3ca193a6ae5a
parent 36945 9bec62c10714
child 38549 d0385f2764d8 
--- a/src/HOL/Statespace/state_fun.ML	Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Tue Jul 27 17:09:35 2010 +0200
@@ -272,7 +272,7 @@
          val ss' = (Simplifier.context ctxt ex_lookup_ss);
          fun prove prop =
            Goal.prove_global thy [] [] prop 
-             (fn _ => record_split_simp_tac [] (K ~1) 1 THEN
+             (fn _ => Record.split_simp_tac [] (K ~1) 1 THEN
                       simp_tac ss' 1);
 
          fun mkeq (swap,Teq,lT,lo,d,n,x,s) i =
isabelle