# HG changeset patch
# User haftmann
# Date 1242398357 -7200
# Node ID 27304e12a412a27f2279b6eaffc829ad0e447c37
# Parent  dae7be64d61476f88ab565ae57501031be91e127
dropped theory Term_Of_Syntax

diff -r dae7be64d614 -r 27304e12a412 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri May 15 16:39:16 2009 +0200
+++ b/src/HOL/IsaMakefile	Fri May 15 16:39:17 2009 +0200
@@ -851,7 +851,7 @@
   ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy			\
   ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
   ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
-  ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy	\
+  ex/Sudoku.thy ex/Tarski.thy \
   ex/Termination.thy ex/Unification.thy ex/document/root.bib		\
   ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
   ex/Predicate_Compile.thy ex/predicate_compile.ML ex/Predicate_Compile_ex.thy
diff -r dae7be64d614 -r 27304e12a412 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri May 15 16:39:16 2009 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri May 15 16:39:17 2009 +0200
@@ -11,7 +11,6 @@
   "Word",
   "Eval_Examples",
   "Quickcheck_Generators",
-  "Term_Of_Syntax",
   "Codegenerator",
   "Codegenerator_Pretty",
   "NormalForm",
diff -r dae7be64d614 -r 27304e12a412 src/HOL/ex/Term_Of_Syntax.thy
--- a/src/HOL/ex/Term_Of_Syntax.thy	Fri May 15 16:39:16 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(*  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 [] ((Binding.name "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 = map_aterms
-    (fn Free (v, _) => error ("illegal free variable in term quotation: " ^ quote v) | t => t)
-      o HOLogic.reflect_term;
-  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