author | wenzelm |
Sun, 17 Sep 2000 22:50:10 +0200 | |
changeset 10013 | be4824b7505d |
parent 10012 | 4961c73b5f60 |
child 10014 | d41ab495ab14 |
--- a/src/HOL/Tools/induct_method.ML Sun Sep 17 22:25:18 2000 +0200 +++ b/src/HOL/Tools/induct_method.ML Sun Sep 17 22:50:10 2000 +0200 @@ -93,7 +93,7 @@ type T = GlobalInductArgs.T; fun init thy = GlobalInduct.get thy; - val print = GlobalInductArgs.print o ProofContext.sign_of; + fun print x = GlobalInductArgs.print (ProofContext.sign_of x); end; structure LocalInduct = ProofDataFun(LocalInductArgs);