changeset 59582 | 0fbed69ff081 |
parent 59498 | 50b60f501b05 |
child 59763 | 56d2c357e6b5 |
--- a/src/Doc/Isar_Ref/Generic.thy Tue Mar 03 19:08:04 2015 +0100 +++ b/src/Doc/Isar_Ref/Generic.thy Wed Mar 04 19:53:18 2015 +0100 @@ -999,7 +999,7 @@ simproc_setup unit ("x::unit") = \<open> fn _ => fn _ => fn ct => - if HOLogic.is_unit (term_of ct) then NONE + if HOLogic.is_unit (Thm.term_of ct) then NONE else SOME (mk_meta_eq @{thm unit_eq}) \<close>