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 27330 1af2598b5f7d
parent 27099 2a91d9575935
child 28308 d4396a28fb29 
--- a/src/HOL/Statespace/state_fun.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -251,7 +251,7 @@
                (trm,trm',vars,_,true)
                 => let
                      val eq1 = Goal.prove ctxt [] [] 
-                                      (list_all (vars,equals sT$trm$trm'))
+                                      (list_all (vars, Logic.mk_equals (trm, trm')))
                                       (fn _ => rtac meta_ext 1 THEN 
                                                simp_tac ss1 1);
                      val eq2 = Simplifier.asm_full_rewrite ss2 (Thm.dest_equals_rhs (cprop_of eq1));
isabelle