src/HOL/FunDef.thy

--- a/src/HOL/FunDef.thy	Thu Mar 12 16:13:14 2009 +0100
+++ b/src/HOL/FunDef.thy	Thu Mar 12 21:29:04 2009 +0100
@@ -314,13 +314,11 @@
 use "Tools/function_package/scnp_reconstruct.ML"
 
 setup {* ScnpReconstruct.setup *}
-(*
-setup {*
+
+ML_val -- "setup inactive"
+{*
   Context.theory_map (FundefCommon.set_termination_prover (ScnpReconstruct.decomp_scnp 
   [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS])) 
 *}
-*)
-
-
 
 end