# HG changeset patch
# User haftmann
# Date 1221644545 -7200
# Node ID 4bf450d50c32d75080fe9af8036423352a735127
# Parent  5710906fd1afda2dc53efca08b53fb9b577a6e84
moved term_of syntax to separate theory

diff -r 5710906fd1af -r 4bf450d50c32 src/HOL/ex/Term_Of_Syntax.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Term_Of_Syntax.thy	Wed Sep 17 11:42:25 2008 +0200
@@ -0,0 +1,60 @@
+(*  Title:      HOL/ex/Term_Of_Syntax.thy
+    ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+header {* Input syntax for term_of functions *}
+
+theory Term_Of_Syntax
+imports Code_Eval
+begin
+
+setup {*
+  Sign.declare_const [] ((Name.binding "rterm_of", @{typ "'a \<Rightarrow> 'b"}), NoSyn)
+  #> snd
+*}
+
+notation (output)
+  rterm_of ("\<guillemotleft>_\<guillemotright>")
+
+locale rterm_syntax =
+  fixes rterm_of_syntax :: "'a \<Rightarrow> 'b" ("\<guillemotleft>_\<guillemotright>")
+
+parse_translation {*
+let
+  fun rterm_of_tr [t] = Lexicon.const @{const_name rterm_of} $ t
+    | rterm_of_tr ts = raise TERM ("rterm_of_tr", ts);
+in
+  [(Syntax.fixedN ^ "rterm_of_syntax", rterm_of_tr)]
+end
+*}
+
+setup {*
+let
+  val subst_rterm_of = Eval.mk_term
+    (fn (v, _) => error ("illegal free variable in term quotation: " ^ quote v))
+    (RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort))));
+  fun subst_rterm_of' (Const (@{const_name rterm_of}, _), [t]) = subst_rterm_of t
+    | subst_rterm_of' (Const (@{const_name rterm_of}, _), _) =
+        error ("illegal number of arguments for " ^ quote @{const_name rterm_of})
+    | subst_rterm_of' (t, ts) = list_comb (t, map (subst_rterm_of' o strip_comb) ts);
+  fun subst_rterm_of'' t = 
+    let
+      val t' = subst_rterm_of' (strip_comb t);
+    in if t aconv t'
+      then NONE
+      else SOME t'
+    end;
+  fun check_rterm_of ts ctxt =
+    let
+      val ts' = map subst_rterm_of'' ts;
+    in if exists is_some ts'
+      then SOME (map2 the_default ts ts', ctxt)
+      else NONE
+    end;
+in
+  Context.theory_map (Syntax.add_term_check 0 "rterm_of" check_rterm_of)
+end;
+*}
+
+end