1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Feb 08 15:49:01 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Feb 08 15:54:01 2010 -0800
     1.3 @@ -180,7 +180,7 @@
     1.4  val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
     1.5  val abs_defin' = iso_locale RS iso_abs_defin';
     1.6  val rep_defin' = iso_locale RS iso_rep_defin';
     1.7 -val iso_rews = map Drule.standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
     1.8 +val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
     1.9  
    1.10  (* ----- generating beta reduction rules from definitions-------------------- *)
    1.11  
    1.12 @@ -263,7 +263,7 @@
    1.13    val exhaust = pg con_appls (mk_trp exh) (K tacs);
    1.14    val _ = trace " Proving casedist...";
    1.15    val casedist =
    1.16 -    Drule.standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
    1.17 +    Drule.export_without_context (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
    1.18  end;
    1.19  
    1.20  local 
    1.21 @@ -554,7 +554,7 @@
    1.22          flat
    1.23            (ListPair.map (distinct c) ((map #1 cs),leqs)) @
    1.24          distincts cs;
    1.25 -  in map Drule.standard (distincts (cons ~~ distincts_le)) end;
    1.26 +  in map Drule.export_without_context (distincts (cons ~~ distincts_le)) end;
    1.27  
    1.28  local 
    1.29    fun pgterm rel con args =
    1.30 @@ -759,7 +759,7 @@
    1.31    fun one_take_apps ((dn, _), cons) = map (one_take_app dn) cons;
    1.32    val take_apps = maps one_take_apps eqs;
    1.33  in
    1.34 -  val take_rews = map Drule.standard
    1.35 +  val take_rews = map Drule.export_without_context
    1.36      (take_stricts @ take_0s @ take_apps);
    1.37  end; (* local *)
    1.38