src/Doc/Isar_Ref/Generic.thy
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>