eliminated dead code;

--- a/src/Pure/Isar/obtain.ML	Wed Sep 30 22:24:57 2009 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed Sep 30 22:25:50 2009 +0200
@@ -215,7 +215,6 @@
     val thy = ProofContext.theory_of ctxt;
     val certT = Thm.ctyp_of thy;
     val cert = Thm.cterm_of thy;
-    val string_of_typ = Syntax.string_of_typ ctxt;
     val string_of_term = setmp show_types true (Syntax.string_of_term ctxt);
 
     fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);

--- a/src/Pure/Isar/proof.ML	Wed Sep 30 22:24:57 2009 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Sep 30 22:25:50 2009 +0200
@@ -581,7 +581,6 @@
   let
     val _ = assert_forward state;
     val thy = theory_of state;
-    val ctxt = context_of state;
 
     val (raw_name_atts, (raw_vars, raw_rhss)) = args |> split_list ||> split_list;
     val name_atts = map (apsnd (map (prep_att thy))) raw_name_atts;
@@ -1008,7 +1007,7 @@
   let
     val _ = assert_backward state;
     val (goal_ctxt, (_, goal)) = find_goal state;
-    val {statement as (kind, propss, prop), messages, using, goal, before_qed, after_qed} = goal;
+    val {statement as (kind, _, prop), messages, using, goal, before_qed, after_qed} = goal;
     val goal_txt = prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt);
 
     val _ = is_relevant state andalso error "Cannot fork relevant proof";

--- a/src/Pure/Isar/specification.ML	Wed Sep 30 22:24:57 2009 +0200
+++ b/src/Pure/Isar/specification.ML	Wed Sep 30 22:25:50 2009 +0200
@@ -136,9 +136,6 @@
   prepare prep_vars parse_prop prep_att do_close
     vars (map single_spec specs) #>> apsnd (map the_spec);
 
-fun prep_specification prep_vars parse_prop prep_att vars specs =
-  prepare prep_vars parse_prop prep_att true [specs];
-
 in
 
 fun check_spec x = prep_spec ProofContext.cert_vars (K I) (K I) true x;

--- a/src/Pure/Syntax/mixfix.ML	Wed Sep 30 22:24:57 2009 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Wed Sep 30 22:25:50 2009 +0200
@@ -128,16 +128,6 @@
 
 fun const_mixfix c mx = (const_name mx c, fix_mixfix c mx);
 
-fun map_mixfix _ NoSyn = NoSyn
-  | map_mixfix f (Mixfix (sy, ps, p)) = Mixfix (f sy, ps, p)
-  | map_mixfix f (Delimfix sy) = Delimfix (f sy)
-  | map_mixfix f (InfixName (sy, p)) = InfixName (f sy, p)
-  | map_mixfix f (InfixlName (sy, p)) = InfixlName (f sy, p)
-  | map_mixfix f (InfixrName (sy, p)) = InfixrName (f sy, p)
-  | map_mixfix f (Binder (sy, p, q)) = Binder (f sy, p, q)
-  | map_mixfix _ Structure = Structure
-  | map_mixfix _ _ = raise Fail ("map_mixfix: illegal occurrence of unnamed infix");
-
 fun mixfix_args NoSyn = 0
   | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy
   | mixfix_args (Delimfix sy) = SynExt.mfix_args sy

--- a/src/Pure/Syntax/syn_trans.ML	Wed Sep 30 22:24:57 2009 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Wed Sep 30 22:25:50 2009 +0200
@@ -155,20 +155,11 @@
   | bigimpl_ast_tr (*"_bigimpl"*) asts = raise Ast.AST ("bigimpl_ast_tr", asts);
 
 
-(* meta conjunction *)
-
-fun conjunction_tr [t, u] = Lexicon.const "Pure.conjunction" $ t $ u
-  | conjunction_tr ts = raise TERM ("conjunction_tr", ts);
-
-
 (* type/term reflection *)
 
 fun type_tr (*"_TYPE"*) [ty] = mk_type ty
   | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts);
 
-fun term_tr [t] = Lexicon.const "Pure.term" $ t
-  | term_tr ts = raise TERM ("term_tr", ts);
-
 
 (* dddot *)
 

--- a/src/Pure/System/isar.ML	Wed Sep 30 22:24:57 2009 +0200
+++ b/src/Pure/System/isar.ML	Wed Sep 30 22:25:50 2009 +0200
@@ -48,7 +48,6 @@
   in edit count (! global_state, ! global_history) end);
 
 fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state);
-fun set_state state = NAMED_CRITICAL "Isar" (fn () => global_state := state);
 
 fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn);
 fun set_exn exn =  NAMED_CRITICAL "Isar" (fn () => global_exn := exn);

--- a/src/Pure/pure_thy.ML	Wed Sep 30 22:24:57 2009 +0200
+++ b/src/Pure/pure_thy.ML	Wed Sep 30 22:25:50 2009 +0200
@@ -239,7 +239,6 @@
 (*** Pure theory syntax and logical content ***)
 
 val typ = SimpleSyntax.read_typ;
-val term = SimpleSyntax.read_term;
 val prop = SimpleSyntax.read_prop;
 
 val typeT = Syntax.typeT;

--- a/src/Pure/simplifier.ML	Wed Sep 30 22:24:57 2009 +0200
+++ b/src/Pure/simplifier.ML	Wed Sep 30 22:25:50 2009 +0200
@@ -287,8 +287,6 @@
 
 val simpN = "simp";
 val congN = "cong";
-val addN = "add";
-val delN = "del";
 val onlyN = "only";
 val no_asmN = "no_asm";
 val no_asm_useN = "no_asm_use";