--- 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;
--- 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 =
--- 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;