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