1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Wed Aug 02 22:26:39 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Wed Aug 02 22:26:40 2006 +0200
     1.3 @@ -113,7 +113,7 @@
     1.4              |> Seq.maps (fn rule' =>
     1.5                CASES (rule_cases rule' cases)
     1.6                  (Tactic.rtac (rename_params_rule false [] rule') i THEN
     1.7 -                  PRIMSEQ (Seq.singleton (ProofContext.exports defs_ctxt ctxt))) st'))))
     1.8 +                  PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
     1.9      THEN_ALL_NEW_CASES InductMethod.rulify_tac
    1.10    end;
    1.11  

     2.1 --- a/src/HOL/Tools/meson.ML	Wed Aug 02 22:26:39 2006 +0200
     2.2 +++ b/src/HOL/Tools/meson.ML	Wed Aug 02 22:26:40 2006 +0200
     2.3 @@ -451,7 +451,7 @@
     2.4  (*Expand all definitions (presumably of Skolem functions) in a proof state.*)
     2.5  fun expand_defs_tac st =
     2.6    let val defs = filter (can dest_equals) (#hyps (crep_thm st))
     2.7 -  in  LocalDefs.def_export false defs st  end;
     2.8 +  in  PRIMITIVE (LocalDefs.def_export false defs) st  end;
     2.9  
    2.10  (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
    2.11  fun MESON cltac i st = 

     3.1 --- a/src/Provers/induct_method.ML	Wed Aug 02 22:26:39 2006 +0200
     3.2 +++ b/src/Provers/induct_method.ML	Wed Aug 02 22:26:40 2006 +0200
     3.3 @@ -404,7 +404,7 @@
     3.4              |> Seq.maps (fn rule' =>
     3.5                CASES (rule_cases rule' cases)
     3.6                  (Tactic.rtac rule' i THEN
     3.7 -                  PRIMSEQ (Seq.singleton (ProofContext.exports defs_ctxt ctxt))) st'))))
     3.8 +                  PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
     3.9      THEN_ALL_NEW_CASES rulify_tac
    3.10    end;
    3.11