# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1313614567 -7200
# Node ID 782a2cd1a8d092b681524f131709b71a5e1f05b2
# Parent  8146b0ad8212bed3226f7392a69b88afc9c7eb97
made same changes as in main branch

diff -r 8146b0ad8212 -r 782a2cd1a8d0 Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Wed Aug 17 21:08:48 2011 +0200
+++ b/Nominal/nominal_function.ML	Wed Aug 17 22:56:07 2011 +0200
@@ -17,7 +17,7 @@
 
   val add_nominal_function_cmd: (binding * string option * mixfix) list ->
     (Attrib.binding * string) list ->  Nominal_Function_Common.nominal_function_config ->
-    (Proof.context -> tactic) -> local_theory -> nominal_info * local_theory
+    (Proof.context -> tactic) -> bool -> local_theory -> nominal_info * local_theory
 
   val nominal_function: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list ->  Nominal_Function_Common.nominal_function_config ->
@@ -25,7 +25,7 @@
 
   val nominal_function_cmd: (binding * string option * mixfix) list ->
     (Attrib.binding * string) list ->  Nominal_Function_Common.nominal_function_config ->
-    local_theory -> Proof.state
+    bool -> local_theory -> Proof.state
 
   val setup : theory -> theory
   val get_congs : Proof.context -> thm list
@@ -135,7 +135,7 @@
   end
 
 (* nominal *)
-fun prepare_nominal_function is_external prep default_constraint fixspec eqns config lthy =
+fun prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy =
   let
     val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
     val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
@@ -181,7 +181,7 @@
           pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
           fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts}
 
-        val _ = Proof_Display.print_consts is_external lthy (K false) (map fst fixes)
+        val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
       in
         (info, 
          lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))
@@ -190,10 +190,10 @@
     ((goal_state, afterqed), lthy')
   end
 
-fun gen_add_nominal_function is_external prep default_constraint fixspec eqns config tac lthy =
+fun gen_add_nominal_function do_print prep default_constraint fixspec eqns config tac lthy =
   let
     val ((goal_state, afterqed), lthy') =
-      prepare_nominal_function is_external prep default_constraint fixspec eqns config lthy
+      prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy
     val pattern_thm =
       case SINGLE (tac lthy') goal_state of
         NONE => error "pattern completeness and compatibility proof failed"
@@ -205,12 +205,13 @@
 
 val add_nominal_function =
   gen_add_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
-val add_nominal_function_cmd = gen_add_nominal_function true Specification.read_spec "_::type"
+fun add_nominal_function_cmd a b c d int = 
+  gen_add_nominal_function int Specification.read_spec "_::type" a b c d
 
-fun gen_nominal_function is_external prep default_constraint fixspec eqns config lthy =
+fun gen_nominal_function do_print prep default_constraint fixspec eqns config lthy =
   let
     val ((goal_state, afterqed), lthy') =
-      prepare_nominal_function is_external prep default_constraint fixspec eqns config lthy
+      prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy
   in
     lthy'
     |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]]
@@ -219,7 +220,9 @@
 
 val nominal_function =
   gen_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
-val nominal_function_cmd = gen_nominal_function true Specification.read_spec "_::type"
+fun nominal_function_cmd a b c int = 
+  gen_nominal_function int Specification.read_spec "_::type" a b c
+
 
 fun add_case_cong n thy =
   let
@@ -271,7 +274,7 @@
 
 (* nominal *)
 val _ =
-  Outer_Syntax.local_theory_to_proof "nominal_primrec" "define general recursive nominal functions"
+  Outer_Syntax.local_theory_to_proof' "nominal_primrec" "define general recursive nominal functions"
   Keyword.thy_goal
   (nominal_function_parser nominal_default_config
      >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config))