--- a/src/HOL/Tools/ComputeHOL.thy Thu Mar 27 14:41:07 2008 +0100
+++ b/src/HOL/Tools/ComputeHOL.thy Thu Mar 27 14:41:09 2008 +0100
@@ -172,12 +172,7 @@
fun prep_thms ths = map (convert_conditions o to_meta_eq) ths
-local
- val sym_HOL = @{thm "HOL.sym"}
- val sym_Pure = @{thm "ProtoPure.symmetric"}
-in
- fun symmetric th = ((sym_HOL OF [th]) handle THM _ => (sym_Pure OF [th]))
-end
+fun symmetric th = @{thm "HOL.sym"} OF [th] handle THM _ => @{thm "Pure.symmetric"} OF [th]
local
val trans_HOL = @{thm "HOL.trans"}