src/Pure/simplifier.ML
changeset 42464 ae16b8abf1a8
parent 42375 774df7c59508
child 42465 1ba52683512a
     1.1 --- a/src/Pure/simplifier.ML	Sat Apr 23 13:00:19 2011 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Sat Apr 23 13:53:09 2011 +0200
     1.3 @@ -58,11 +58,11 @@
     1.4    val cong_add: attribute
     1.5    val cong_del: attribute
     1.6    val map_simpset: (simpset -> simpset) -> theory -> theory
     1.7 -  val get_simproc: Context.generic -> xstring -> simproc
     1.8 -  val def_simproc: {name: string, lhss: string list,
     1.9 +  val get_simproc: Proof.context -> xstring * Position.T -> simproc
    1.10 +  val def_simproc: {name: binding, lhss: term list,
    1.11      proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
    1.12      local_theory -> local_theory
    1.13 -  val def_simproc_i: {name: string, lhss: term list,
    1.14 +  val def_simproc_cmd: {name: binding, lhss: string list,
    1.15      proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
    1.16      local_theory -> local_theory
    1.17    val cong_modifiers: Method.modifier parser list
    1.18 @@ -162,27 +162,28 @@
    1.19  
    1.20  (* get simprocs *)
    1.21  
    1.22 -fun get_simproc context xname =
    1.23 +fun get_simproc ctxt (xname, pos) =
    1.24    let
    1.25 -    val (space, tab) = Simprocs.get context;
    1.26 +    val (space, tab) = Simprocs.get (Context.Proof ctxt);
    1.27      val name = Name_Space.intern space xname;
    1.28    in
    1.29      (case Symtab.lookup tab name of
    1.30 -      SOME proc => proc
    1.31 +      SOME proc => (Context_Position.report ctxt pos (Name_Space.markup space name); proc)
    1.32      | NONE => error ("Undefined simplification procedure: " ^ quote name))
    1.33    end;
    1.34  
    1.35 -val _ = ML_Antiquote.value "simproc" (Scan.lift Args.name >> (fn name =>
    1.36 -  "Simplifier.get_simproc (ML_Context.the_generic_context ()) " ^ ML_Syntax.print_string name));
    1.37 +val _ =
    1.38 +  ML_Antiquote.value "simproc" (Scan.lift (Parse.position Args.name) >> (fn x =>
    1.39 +    "Simplifier.get_simproc (ML_Context.the_local_context ()) " ^
    1.40 +      ML_Syntax.print_pair ML_Syntax.print_string  ML_Syntax.print_position x));
    1.41  
    1.42  
    1.43  (* define simprocs *)
    1.44  
    1.45  local
    1.46  
    1.47 -fun gen_simproc prep {name, lhss, proc, identifier} lthy =
    1.48 +fun gen_simproc prep {name = b, lhss, proc, identifier} lthy =
    1.49    let
    1.50 -    val b = Binding.name name;
    1.51      val naming = Local_Theory.naming_of lthy;
    1.52      val simproc = make_simproc
    1.53        {name = Name_Space.full_name naming b,
    1.54 @@ -211,8 +212,8 @@
    1.55  
    1.56  in
    1.57  
    1.58 -val def_simproc = gen_simproc Syntax.read_terms;
    1.59 -val def_simproc_i = gen_simproc Syntax.check_terms;
    1.60 +val def_simproc = gen_simproc Syntax.check_terms;
    1.61 +val def_simproc_cmd = gen_simproc Syntax.read_terms;
    1.62  
    1.63  end;
    1.64  
    1.65 @@ -310,7 +311,7 @@
    1.66  val simproc_att =
    1.67    Scan.peek (fn context =>
    1.68      add_del :|-- (fn decl =>
    1.69 -      Scan.repeat1 (Args.named_attribute (decl o get_simproc context))
    1.70 +      Scan.repeat1 (Args.named_attribute (decl o get_simproc (Context.proof_of context)))
    1.71        >> (Library.apply o map Morphism.form)));
    1.72  
    1.73  end;