Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/HOL/Library/reflection.ML
changeset 36945 9bec62c10714
parent 36692 54b64d4ad524
child 37117 59cee8807c29 
     1.1 --- a/src/HOL/Library/reflection.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/HOL/Library/reflection.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4                               (AList.update Type.could_unify (HOLogic.listT xT, ((x::bsT), atsT)) bds))
     1.5                 in (([(ta, ctxt')],
     1.6                      fn ([th], bds) =>
     1.7 -                      (hd (Variable.export ctxt' ctxt [(forall_intr (cert x) th) COMP allI]),
     1.8 +                      (hd (Variable.export ctxt' ctxt [(Thm.forall_intr (cert x) th) COMP allI]),
     1.9                         let val (bsT,asT) = the(AList.lookup Type.could_unify bds (HOLogic.listT xT))
    1.10                         in AList.update Type.could_unify (HOLogic.listT xT,(tl bsT,asT)) bds
    1.11                         end)),
isabelle