changeset 53651 | ee90c67502c9 |
parent 52883 | 0a7c97c76f46 |
child 55454 | 6ea67a791108 |
--- a/src/HOL/Tools/Lifting/lifting_util.ML Mon Sep 16 11:54:57 2013 +0200 +++ b/src/HOL/Tools/Lifting/lifting_util.ML Mon Sep 16 15:30:17 2013 +0200 @@ -28,7 +28,7 @@ val relation_types: typ -> typ * typ val mk_HOL_eq: thm -> thm val safe_HOL_meta_eq: thm -> thm -end; +end structure Lifting_Util: LIFTING_UTIL = @@ -110,4 +110,4 @@ fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r -end; +end