# HG changeset patch
# User clasohm
# Date 829905185 -7200
# Node ID 5183de4c496dfbe83cf3d0ac1aa58a0363c8de13
# Parent  e5737154d9bf731dcae6d371189bf6b2d1197d9c
removed assignment of HOL_ss to simpset

diff -r e5737154d9bf -r 5183de4c496d src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Fri Apr 19 11:12:05 1996 +0200
+++ b/src/HOL/Fun.ML	Fri Apr 19 11:13:05 1996 +0200
@@ -6,8 +6,6 @@
 Lemmas about functions.
 *)
 
-simpset := HOL_ss;
-
 goal Fun.thy "(f = g) = (!x. f(x)=g(x))";
 by (rtac iffI 1);
 by (Asm_simp_tac 1);