# HG changeset patch
# User wenzelm
# Date 1154550400 -7200
# Node ID 8ff4a0ea49b210fcdaf3173d7951e221289f42f4
# Parent  8cbcb46c3c099290bdc96144c5c45ff768777377
simplified Assumption/ProofContext.export;

diff -r 8cbcb46c3c09 -r 8ff4a0ea49b2 src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Wed Aug 02 22:26:39 2006 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML	Wed Aug 02 22:26:40 2006 +0200
@@ -113,7 +113,7 @@
             |> Seq.maps (fn rule' =>
               CASES (rule_cases rule' cases)
                 (Tactic.rtac (rename_params_rule false [] rule') i THEN
-                  PRIMSEQ (Seq.singleton (ProofContext.exports defs_ctxt ctxt))) st'))))
+                  PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
     THEN_ALL_NEW_CASES InductMethod.rulify_tac
   end;
 
diff -r 8cbcb46c3c09 -r 8ff4a0ea49b2 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Wed Aug 02 22:26:39 2006 +0200
+++ b/src/HOL/Tools/meson.ML	Wed Aug 02 22:26:40 2006 +0200
@@ -451,7 +451,7 @@
 (*Expand all definitions (presumably of Skolem functions) in a proof state.*)
 fun expand_defs_tac st =
   let val defs = filter (can dest_equals) (#hyps (crep_thm st))
-  in  LocalDefs.def_export false defs st  end;
+  in  PRIMITIVE (LocalDefs.def_export false defs) st  end;
 
 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
 fun MESON cltac i st = 
diff -r 8cbcb46c3c09 -r 8ff4a0ea49b2 src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Wed Aug 02 22:26:39 2006 +0200
+++ b/src/Provers/induct_method.ML	Wed Aug 02 22:26:40 2006 +0200
@@ -404,7 +404,7 @@
             |> Seq.maps (fn rule' =>
               CASES (rule_cases rule' cases)
                 (Tactic.rtac rule' i THEN
-                  PRIMSEQ (Seq.singleton (ProofContext.exports defs_ctxt ctxt))) st'))))
+                  PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
     THEN_ALL_NEW_CASES rulify_tac
   end;