# HG changeset patch
# User berghofe
# Date 1150128945 -7200
# Node ID 7408a891424ebd7beefb66073f189a7ae62ae6f0
# Parent  ee5cd747c10afb52924c840f9a72dd49d1f630fd
Removed comments around declaration of fresh_guess method.

diff -r ee5cd747c10a -r 7408a891424e src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Mon Jun 12 17:16:03 2006 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Mon Jun 12 18:15:45 2006 +0200
@@ -2929,7 +2929,6 @@
   {* finite_gs_meth_debug *}
   {* tactic for deciding whether something has finite support including debuging facilities *}
 
-(* FIXME: this code has not yet been checked in
 method_setup fresh_guess =
   {* fresh_gs_meth *}
   {* tactic for deciding whether an atom is fresh for something*}
@@ -2937,6 +2936,5 @@
 method_setup fresh_guess_debug =
   {* fresh_gs_meth_debug *}
   {* tactic for deciding whether an atom is fresh for something including debuging facilities *}
-*)
 
 end