src/Pure/simplifier.ML
changeset 27338 2cd6c60cc10b
parent 27021 4593b9f4ba42
child 28074 90adbbf03187
     1.1 --- a/src/Pure/simplifier.ML	Tue Jun 24 19:43:12 2008 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Tue Jun 24 19:43:14 2008 +0200
     1.3 @@ -133,8 +133,8 @@
     1.4  
     1.5  fun local_simpset_of ctxt = MetaSimplifier.context ctxt (get_ss (Context.Proof ctxt));
     1.6  
     1.7 -val _ = ML_Context.value_antiq "simpset"
     1.8 -  (Scan.succeed ("simpset", "Simplifier.local_simpset_of (ML_Context.the_local_context ())"));
     1.9 +val _ = ML_Antiquote.value "simpset"
    1.10 +  (Scan.succeed "Simplifier.local_simpset_of (ML_Context.the_local_context ())");
    1.11  
    1.12  
    1.13  
    1.14 @@ -167,9 +167,8 @@
    1.15      | NONE => error ("Undefined simplification procedure: " ^ quote name))
    1.16    end;
    1.17  
    1.18 -val _ = ML_Context.value_antiq "simproc" (Scan.lift Args.name >> (fn name =>
    1.19 -  ("simproc",
    1.20 -    "Simplifier.get_simproc (ML_Context.the_generic_context ()) " ^ ML_Syntax.print_string name)));
    1.21 +val _ = ML_Antiquote.value "simproc" (Scan.lift Args.name >> (fn name =>
    1.22 +  "Simplifier.get_simproc (ML_Context.the_generic_context ()) " ^ ML_Syntax.print_string name));
    1.23  
    1.24  
    1.25  (* define simprocs *)