Toplevel.local_theory_to_proof: proper target;
authorwenzelm
Thu Oct 12 22:57:20 2006 +0200 (2006-10-12)
changeset 2100054c42dfbcafa
parent 20999 9131d8e96dba
child 21001 408f3a1cef2e
Toplevel.local_theory_to_proof: proper target;
src/HOL/Tools/function_package/fundef_package.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Oct 12 22:57:15 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Oct 12 22:57:20 2006 +0200
     1.3 @@ -185,20 +185,20 @@
     1.4  val statements_ow = or_list1 statement_ow
     1.5  
     1.6  
     1.7 -fun local_theory_to_proof f =
     1.8 -    Toplevel.theory_to_proof (f o TheoryTarget.init NONE)
     1.9 -
    1.10  val functionP =
    1.11    OuterSyntax.command "function" "define general recursive functions" K.thy_goal
    1.12    ((config_parser -- P.opt_locale_target -- P.fixes --| P.$$$ "where" -- statements_ow)
    1.13       >> (fn (((config, target), fixes), statements) =>
    1.14 -            Toplevel.print o local_theory_to_proof (add_fundef fixes statements config)));
    1.15 +            Toplevel.print o
    1.16 +            Toplevel.local_theory_to_proof target (add_fundef fixes statements config)));
    1.17  
    1.18  
    1.19  val terminationP =
    1.20    OuterSyntax.command "termination" "prove termination of a recursive function" K.thy_goal
    1.21 -  (Scan.option P.name
    1.22 -    >> (fn name => Toplevel.print o local_theory_to_proof (fundef_setup_termination_proof name)));
    1.23 +  (P.opt_locale_target -- Scan.option P.name
    1.24 +    >> (fn (target, name) =>
    1.25 +           Toplevel.print o
    1.26 +           Toplevel.local_theory_to_proof target (fundef_setup_termination_proof name)));
    1.27  
    1.28  
    1.29  val _ = OuterSyntax.add_parsers [functionP];