src/HOL/Tools/TFL/tfl.ML
changeset 36945 9bec62c10714
parent 36692 54b64d4ad524
child 38549 d0385f2764d8
     1.1 --- a/src/HOL/Tools/TFL/tfl.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -556,8 +556,8 @@
     1.4                             else ()
     1.5       val f_free = Free (fid, fastype_of f)  (*'cos f is a Const*)
     1.6       val SV' = map tych SV;
     1.7 -     val SVrefls = map reflexive SV'
     1.8 -     val def0 = (fold (fn x => fn th => R.rbeta(combination th x))
     1.9 +     val SVrefls = map Thm.reflexive SV'
    1.10 +     val def0 = (fold (fn x => fn th => R.rbeta(Thm.combination th x))
    1.11                     SVrefls def)
    1.12                  RS meta_eq_to_obj_eq
    1.13       val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0