Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned signature;
authorwenzelm
Thu, 10 Nov 2011 17:47:25 +0100
changeset 45444 ac069060e08a
parent 45443 c8a9a5e577bd
child 45445 41e641a870de
tuned signature;
src/Pure/Isar/overloading.ML file | annotate | diff | comparison | revisions
src/Pure/Syntax/syntax_phases.ML file | annotate | diff | comparison | revisions
src/Tools/adhoc_overloading.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/overloading.ML	Thu Nov 10 17:41:36 2011 +0100
+++ b/src/Pure/Isar/overloading.ML	Thu Nov 10 17:47:25 2011 +0100
@@ -114,8 +114,8 @@
 
 val activate_improvable_syntax =
   Context.proof_map
-    (Syntax_Phases.context_term_check 0 "improvement" improve_term_check
-    #> Syntax_Phases.context_term_uncheck 0 "improvement" improve_term_uncheck)
+    (Syntax_Phases.term_check' 0 "improvement" improve_term_check
+    #> Syntax_Phases.term_uncheck' 0 "improvement" improve_term_uncheck)
   #> set_primary_constraints;
 
 
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Nov 10 17:41:36 2011 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Nov 10 17:47:25 2011 +0100
@@ -14,18 +14,6 @@
   val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
   val term_of_typ: Proof.context -> typ -> term
   val print_checks: Proof.context -> unit
-  val context_typ_check: int -> string ->
-    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
-    Context.generic -> Context.generic
-  val context_term_check: int -> string ->
-    (term list -> Proof.context -> (term list * Proof.context) option) ->
-    Context.generic -> Context.generic
-  val context_typ_uncheck: int -> string ->
-    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
-    Context.generic -> Context.generic
-  val context_term_uncheck: int -> string ->
-    (term list -> Proof.context -> (term list * Proof.context) option) ->
-    Context.generic -> Context.generic
   val typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
     Context.generic -> Context.generic
   val term_check: int -> string -> (Proof.context -> term list -> term list) ->
@@ -34,6 +22,18 @@
     Context.generic -> Context.generic
   val term_uncheck: int -> string -> (Proof.context -> term list -> term list) ->
     Context.generic -> Context.generic
+  val typ_check': int -> string ->
+    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
+    Context.generic -> Context.generic
+  val term_check': int -> string ->
+    (term list -> Proof.context -> (term list * Proof.context) option) ->
+    Context.generic -> Context.generic
+  val typ_uncheck': int -> string ->
+    (typ list -> Proof.context -> (typ list * Proof.context) option) ->
+    Context.generic -> Context.generic
+  val term_uncheck': int -> string ->
+    (term list -> Proof.context -> (term list * Proof.context) option) ->
+    Context.generic -> Context.generic
 end
 
 structure Syntax_Phases: SYNTAX_PHASES =
@@ -763,15 +763,15 @@
 
 in
 
-fun context_typ_check stage = context_check apfst (stage, false);
-fun context_term_check stage = context_check apsnd (stage, false);
-fun context_typ_uncheck stage = context_check apfst (stage, true);
-fun context_term_uncheck stage = context_check apsnd (stage, true);
+fun typ_check' stage = context_check apfst (stage, false);
+fun term_check' stage = context_check apsnd (stage, false);
+fun typ_uncheck' stage = context_check apfst (stage, true);
+fun term_uncheck' stage = context_check apsnd (stage, true);
 
-fun typ_check key name f = context_typ_check key name (simple_check (op =) f);
-fun term_check key name f = context_term_check key name (simple_check (op aconv) f);
-fun typ_uncheck key name f = context_typ_uncheck key name (simple_check (op =) f);
-fun term_uncheck key name f = context_term_uncheck key name (simple_check (op aconv) f);
+fun typ_check key name f = typ_check' key name (simple_check (op =) f);
+fun term_check key name f = term_check' key name (simple_check (op aconv) f);
+fun typ_uncheck key name f = typ_uncheck' key name (simple_check (op =) f);
+fun term_uncheck key name f = term_uncheck' key name (simple_check (op aconv) f);
 
 end;
 
--- a/src/Tools/adhoc_overloading.ML	Thu Nov 10 17:41:36 2011 +0100
+++ b/src/Tools/adhoc_overloading.ML	Thu Nov 10 17:47:25 2011 +0100
@@ -132,8 +132,8 @@
 (* setup *)
 
 val setup = Context.theory_map
-  (Syntax_Phases.context_term_check 0 "adhoc_overloading" check
-   #> Syntax_Phases.context_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
-   #> Syntax_Phases.context_term_uncheck 0 "adhoc_overloading" uncheck);
+  (Syntax_Phases.term_check' 0 "adhoc_overloading" check
+   #> Syntax_Phases.term_check' 1 "adhoc_overloading_unresolved_check" reject_unresolved
+   #> Syntax_Phases.term_uncheck' 0 "adhoc_overloading" uncheck);
 
 end;
isabelle