src/HOL/HOL.thy
changeset 58956 a816aa3ff391
parent 58889 5b7a9633cfa8
child 58957 c9e744ea8a38
     1.1 --- a/src/HOL/HOL.thy	Sun Nov 09 11:05:20 2014 +0100
     1.2 +++ b/src/HOL/HOL.thy	Sun Nov 09 14:08:00 2014 +0100
     1.3 @@ -274,7 +274,7 @@
     1.4  apply (rule refl)
     1.5  done
     1.6  
     1.7 -ML {* val cong_tac = Cong_Tac.cong_tac @{thm cong} *}
     1.8 +ML {* fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong} *}
     1.9  
    1.10  
    1.11  subsubsection {* Equality of booleans -- iff *}