src/HOL/FunDef.thy

--- a/src/HOL/FunDef.thy	Wed Apr 28 10:31:15 2010 +0200
+++ b/src/HOL/FunDef.thy	Wed Apr 28 11:52:04 2010 +0200
@@ -314,8 +314,8 @@
 
 ML_val -- "setup inactive"
 {*
-  Context.theory_map (Function_Common.set_termination_prover (ScnpReconstruct.decomp_scnp 
-  [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS])) 
+  Context.theory_map (Function_Common.set_termination_prover
+    (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))
 *}
 
 end