src/Provers/hypsubst.ML
changeset 36945 9bec62c10714
parent 36543 0e7fc5bf38de
child 39297 4f9e933a16e2
     1.1 --- a/src/Provers/hypsubst.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/Provers/hypsubst.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -143,7 +143,7 @@
     1.4      [ if inspect_pair bnd false (Data.dest_eq
     1.5                                     (Data.dest_Trueprop (#prop (rep_thm th))))
     1.6        then th RS Data.eq_reflection
     1.7 -      else symmetric(th RS Data.eq_reflection) (*reorient*) ]
     1.8 +      else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
     1.9      handle TERM _ => [] | Match => [];
    1.10  
    1.11  local