# HG changeset patch
# User berghofe
# Date 1208336266 -7200
# Node ID 447f4872b7eef413a4056760f3e98178bebdf305
# Parent  a3ae088dc20f07e6e8717c5aba5320858a7c7247
Added add_primrec_global and add_primrec_overloaded functions (thanks to Markus).

diff -r a3ae088dc20f -r 447f4872b7ee src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Wed Apr 16 10:50:37 2008 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Wed Apr 16 10:57:46 2008 +0200
@@ -10,6 +10,11 @@
 sig
   val add_primrec: (string * typ option * mixfix) list ->
     ((bstring * Attrib.src list) * term) list -> local_theory -> thm list * local_theory
+  val add_primrec_global: (string * typ option * mixfix) list ->
+    ((bstring * Attrib.src list) * term) list -> theory -> thm list * theory
+  val add_primrec_overloaded: (string * (string * typ) * bool) list ->
+    (string * typ option * mixfix) list ->
+    ((bstring * Attrib.src list) * term) list -> theory -> thm list * theory
 end;
 
 structure PrimrecPackage : PRIMREC_PACKAGE =
@@ -268,6 +273,20 @@
 
 end;
 
+fun add_primrec_global fixes specs thy =
+  let
+    val lthy = TheoryTarget.init NONE thy;
+    val (simps, lthy') = add_primrec fixes specs lthy;
+    val simps' = ProofContext.export lthy' lthy simps;
+  in (simps', ProofContext.theory_of (LocalTheory.exit lthy')) end;
+
+fun add_primrec_overloaded ops fixes specs thy =
+  let
+    val lthy = TheoryTarget.overloading ops thy;
+    val (simps, lthy') = add_primrec fixes specs lthy;
+    val simps' = ProofContext.export lthy' lthy simps;
+  in (simps', ProofContext.theory_of (LocalTheory.exit lthy')) end;
+
 
 (* outer syntax *)