src/HOL/Tools/Function/fun.ML
changeset 36519 46bf776a81e0
parent 34232 36a2a3029fd3
child 36521 73ed9f18fdd3
     1.1 --- a/src/HOL/Tools/Function/fun.ML	Wed Apr 28 09:21:48 2010 +0200
     1.2 +++ b/src/HOL/Tools/Function/fun.ML	Wed Apr 28 09:48:22 2010 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4       SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
     1.5  
     1.6  fun termination_by method int =
     1.7 -  Function.termination_proof NONE
     1.8 +  Function.termination NONE
     1.9    #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int
    1.10  
    1.11  fun mk_catchall fixes arity_of =
    1.12 @@ -155,8 +155,8 @@
    1.13    |> Local_Theory.restore
    1.14    |> termination_by (Function_Common.get_termination_prover lthy) int
    1.15  
    1.16 -val add_fun = gen_fun Function.add_function
    1.17 -val add_fun_cmd = gen_fun Function.add_function_cmd
    1.18 +val add_fun = gen_fun Function.function
    1.19 +val add_fun_cmd = gen_fun Function.function_cmd
    1.20  
    1.21  
    1.22