src/HOL/Statespace/state_fun.ML
changeset 36945 9bec62c10714
parent 36148 4ddcc2b07891
child 38012 3ca193a6ae5a
     1.1 --- a/src/HOL/Statespace/state_fun.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/HOL/Statespace/state_fun.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -245,7 +245,7 @@
     1.4                                        (fn _ => rtac meta_ext 1 THEN 
     1.5                                                 simp_tac ss1 1);
     1.6                       val eq2 = Simplifier.asm_full_rewrite ss2 (Thm.dest_equals_rhs (cprop_of eq1));
     1.7 -                   in SOME (transitive eq1 eq2) end
     1.8 +                   in SOME (Thm.transitive eq1 eq2) end
     1.9               | _ => NONE)
    1.10           end
    1.11         | _ => NONE));