1.1 --- a/src/Provers/clasimp.ML	Tue Jan 10 19:33:27 2006 +0100
     1.2 +++ b/src/Provers/clasimp.ML	Tue Jan 10 19:33:29 2006 +0100
     1.3 @@ -154,6 +154,14 @@
     1.4       delss (ss, [th]))
     1.5    end;
     1.6  
     1.7 +fun modifier att (x, ths) =
     1.8 +  fst (Thm.applys_attributes [att] (x, rev ths));
     1.9 +
    1.10 +fun addXIs which = modifier (which (ContextRules.intro_query NONE));
    1.11 +fun addXEs which = modifier (which (ContextRules.elim_query NONE));
    1.12 +fun addXDs which = modifier (which (ContextRules.dest_query NONE));
    1.13 +fun delXs which = modifier (which ContextRules.rule_del);
    1.14 +
    1.15  in
    1.16  
    1.17  val op addIffs =
    1.18 @@ -168,21 +176,21 @@
    1.19  
    1.20  fun addIffs_global (thy, ths) =
    1.21    Library.foldl (addIff
    1.22 -    (ContextRules.addXEs_global, ContextRules.addXIs_global)
    1.23 -    (ContextRules.addXEs_global, ContextRules.addXIs_global) #1)
    1.24 +    (addXEs Attrib.theory, addXIs Attrib.theory)
    1.25 +    (addXEs Attrib.theory, addXIs Attrib.theory) #1)
    1.26    ((thy, ()), ths) |> #1;
    1.27  
    1.28  fun addIffs_local (ctxt, ths) =
    1.29    Library.foldl (addIff
    1.30 -    (ContextRules.addXEs_local, ContextRules.addXIs_local)
    1.31 -    (ContextRules.addXEs_local, ContextRules.addXIs_local) #1)
    1.32 +    (addXEs Attrib.context, addXIs Attrib.context)
    1.33 +    (addXEs Attrib.context, addXIs Attrib.context) #1)
    1.34    ((ctxt, ()), ths) |> #1;
    1.35  
    1.36  fun delIffs_global (thy, ths) =
    1.37 -  Library.foldl (delIff ContextRules.delrules_global #1) ((thy, ()), ths) |> #1;
    1.38 +  Library.foldl (delIff (delXs Attrib.theory) #1) ((thy, ()), ths) |> #1;
    1.39  
    1.40  fun delIffs_local (ctxt, ths) =
    1.41 -  Library.foldl (delIff ContextRules.delrules_local #1) ((ctxt, ()), ths) |> #1;
    1.42 +  Library.foldl (delIff (delXs Attrib.context) #1) ((ctxt, ()), ths) |> #1;
    1.43  
    1.44  end;
    1.45