# HG changeset patch
# User huffman
# Date 1290005363 28800
# Node ID 1c0b5bfa52a174bd952b25c1cd5e27b7b09b4c08
# Parent  b994d855dbd28e1dd9ceb382258453ffe39d3cfa# Parent  5a2b0b817eca0643f9402b7fe04aafe2cedac242
merged

diff -r b994d855dbd2 -r 1c0b5bfa52a1 Admin/makedist
--- a/Admin/makedist	Tue Nov 16 16:36:57 2010 -0800
+++ b/Admin/makedist	Wed Nov 17 06:49:23 2010 -0800
@@ -108,7 +108,7 @@
 
 if [ -z "$RELEASE" ]; then
   DISTNAME="Isabelle_$DATE"
-  DISTVERSION="Isabelle repository snapshot $IDENT ($DATE)"
+  DISTVERSION="Isabelle repository snapshot $IDENT $DATE"
 else
   DISTNAME="$RELEASE"
   DISTVERSION="$DISTNAME: $DISTDATE"
diff -r b994d855dbd2 -r 1c0b5bfa52a1 Isabelle
--- a/Isabelle	Tue Nov 16 16:36:57 2010 -0800
+++ b/Isabelle	Wed Nov 17 06:49:23 2010 -0800
@@ -24,6 +24,6 @@
 [ -e "$ISABELLE_HOME/Admin/build" ] && "$ISABELLE_HOME/Admin/build" jars
 
 CLASSPATH="$(jvmpath "$CLASSPATH")"
-exec "$ISABELLE_JAVA" \
+exec "$ISABELLE_TOOL" java \
   "-Disabelle.home=$(jvmpath "$ISABELLE_HOME")" \
   -jar "$(jvmpath "$ISABELLE_HOME/lib/classes/isabelle-scala.jar")" "$@"
diff -r b994d855dbd2 -r 1c0b5bfa52a1 NEWS
--- a/NEWS	Tue Nov 16 16:36:57 2010 -0800
+++ b/NEWS	Wed Nov 17 06:49:23 2010 -0800
@@ -355,6 +355,9 @@
     cvc3_options
     yices_options
 
+* Boogie output files (.b2i files) need to be declared in the
+theory header.
+
 * Removed [split_format ... and ... and ...] version of
 [split_format].  Potential INCOMPATIBILITY.
 
diff -r b994d855dbd2 -r 1c0b5bfa52a1 doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Tue Nov 16 16:36:57 2010 -0800
+++ b/doc-src/System/Thy/Basics.thy	Wed Nov 17 06:49:23 2010 -0800
@@ -309,12 +309,18 @@
   The root of component initialization is @{setting ISABELLE_HOME}
   itself.  After initializing all of its sub-components recursively,
   @{setting ISABELLE_HOME_USER} is included in the same manner (if
-  that directory exists).  Thus users can easily add private
-  components to @{verbatim "$ISABELLE_HOME_USER/etc/components"}.
-
-  It is also possible to initialize components programmatically via
-  the \verb,init_component, shell function, say within the
-  \verb,settings, script of another component.
+  that directory exists).  This allows to install private components
+  via @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is
+  often more convenient to do that programmatically via the
+  \verb,init_component, shell function in the \verb,etc/settings,
+  script of \verb,$ISABELLE_HOME_USER, (or any other component
+  directory).  For example:
+  \begin{verbatim}
+  if [ -d "$HOME/screwdriver-2.0" ]
+  then
+    init_component "$HOME/screwdriver-2.0"
+  else
+  \end{verbatim}
 *}
 
 
diff -r b994d855dbd2 -r 1c0b5bfa52a1 doc-src/System/Thy/document/Basics.tex
--- a/doc-src/System/Thy/document/Basics.tex	Tue Nov 16 16:36:57 2010 -0800
+++ b/doc-src/System/Thy/document/Basics.tex	Wed Nov 17 06:49:23 2010 -0800
@@ -318,12 +318,18 @@
   The root of component initialization is \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}
   itself.  After initializing all of its sub-components recursively,
   \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} is included in the same manner (if
-  that directory exists).  Thus users can easily add private
-  components to \verb|$ISABELLE_HOME_USER/etc/components|.
-
-  It is also possible to initialize components programmatically via
-  the \verb,init_component, shell function, say within the
-  \verb,settings, script of another component.%
+  that directory exists).  This allows to install private components
+  via \verb|$ISABELLE_HOME_USER/etc/components|, although it is
+  often more convenient to do that programmatically via the
+  \verb,init_component, shell function in the \verb,etc/settings,
+  script of \verb,$ISABELLE_HOME_USER, (or any other component
+  directory).  For example:
+  \begin{verbatim}
+  if [ -d "$HOME/screwdriver-2.0" ]
+  then
+    init_component "$HOME/screwdriver-2.0"
+  else
+  \end{verbatim}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r b994d855dbd2 -r 1c0b5bfa52a1 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Tue Nov 16 16:36:57 2010 -0800
+++ b/etc/isar-keywords.el	Wed Nov 17 06:49:23 2010 -0800
@@ -81,6 +81,7 @@
     "display_drafts"
     "domain"
     "domain_isomorphism"
+    "domaindef"
     "done"
     "enable_pr"
     "end"
@@ -207,7 +208,6 @@
     "refute_params"
     "remove_thy"
     "rep_datatype"
-    "repdef"
     "schematic_corollary"
     "schematic_lemma"
     "schematic_theorem"
@@ -247,6 +247,7 @@
     "txt"
     "txt_raw"
     "typ"
+    "type_mapper"
     "type_notation"
     "typed_print_translation"
     "typedecl"
@@ -460,6 +461,7 @@
     "defs"
     "domain"
     "domain_isomorphism"
+    "domaindef"
     "equivariance"
     "extract"
     "extract_type"
@@ -501,7 +503,6 @@
     "recdef"
     "record"
     "refute_params"
-    "repdef"
     "setup"
     "simproc_setup"
     "sledgehammer_params"
@@ -548,6 +549,7 @@
     "sublocale"
     "termination"
     "theorem"
+    "type_mapper"
     "typedef"))
 
 (defconst isar-keywords-qed
diff -r b994d855dbd2 -r 1c0b5bfa52a1 etc/settings
--- a/etc/settings	Tue Nov 16 16:36:57 2010 -0800
+++ b/etc/settings	Wed Nov 17 06:49:23 2010 -0800
@@ -55,7 +55,11 @@
 ### JVM components (Scala or Java)
 ###
 
-ISABELLE_JAVA="java"
+if [ -n "$JAVA_HOME" ]; then
+  ISABELLE_JAVA="$JAVA_HOME/bin/java"
+else
+  ISABELLE_JAVA="java"
+fi
 
 classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
 
diff -r b994d855dbd2 -r 1c0b5bfa52a1 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Tue Nov 16 16:36:57 2010 -0800
+++ b/lib/scripts/getsettings	Wed Nov 17 06:49:23 2010 -0800
@@ -72,6 +72,7 @@
       CLASSPATH="$CLASSPATH:$X"
     fi
   done
+  export CLASSPATH
 }
 
 #arrays
@@ -90,6 +91,13 @@
 function init_component ()
 {
   local COMPONENT="$1"
+  case "$COMPONENT" in
+    /*) ;;
+    *)
+      echo >&2 "Absolute component path required: \"$COMPONENT\""
+      exit 2
+      ;;
+  esac
 
   if [ ! -d "$COMPONENT" ]; then
     echo >&2 "Bad Isabelle component: \"$COMPONENT\""
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Wed Nov 17 06:49:23 2010 -0800
@@ -80,7 +80,7 @@
 *}
 
 
-boogie_open "Boogie_Dijkstra"
+boogie_open "Boogie_Dijkstra.b2i"
 
 declare [[smt_certificates="Boogie_Dijkstra.certs"]]
 declare [[smt_fixed=true]]
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/Boogie/Examples/Boogie_Max.thy
--- a/src/HOL/Boogie/Examples/Boogie_Max.thy	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Boogie/Examples/Boogie_Max.thy	Wed Nov 17 06:49:23 2010 -0800
@@ -37,7 +37,7 @@
 \end{verbatim}
 *}
 
-boogie_open "Boogie_Max"
+boogie_open "Boogie_Max.b2i"
 
 declare [[smt_certificates="Boogie_Max.certs"]]
 declare [[smt_fixed=true]]
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy
--- a/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy	Wed Nov 17 06:49:23 2010 -0800
@@ -37,7 +37,7 @@
 \end{verbatim}
 *}
 
-boogie_open "Boogie_Max"
+boogie_open "Boogie_Max.b2i"
 
 boogie_status -- {* gives an overview of all verification conditions *}
 
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/Boogie/Examples/VCC_Max.thy
--- a/src/HOL/Boogie/Examples/VCC_Max.thy	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy	Wed Nov 17 06:49:23 2010 -0800
@@ -45,7 +45,7 @@
 \end{verbatim}
 *}
 
-boogie_open (quiet) "VCC_Max"
+boogie_open (quiet) "VCC_Max.b2i"
 
 declare [[smt_certificates="VCC_Max.certs"]]
 declare [[smt_fixed=true]]
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/Boogie/Tools/boogie_commands.ML
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Wed Nov 17 06:49:23 2010 -0800
@@ -17,8 +17,11 @@
 fun boogie_open ((quiet, base_name), offsets) thy =
   let
     val ext = "b2i"
-    fun add_ext path = path |> snd (Path.split_ext path) <> ext ? Path.ext ext
-    val base_path = add_ext (Path.explode base_name)
+    fun check_ext path = snd (Path.split_ext path) = ext orelse
+      error ("Bad file ending of file " ^ quote (Path.implode path) ^ ", " ^
+        "expected file ending " ^ quote ext)
+
+    val base_path = Path.explode base_name |> tap check_ext
     val (full_path, _) =
       Thy_Load.check_file [Thy_Load.master_directory thy] base_path
 
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/HOL.thy	Wed Nov 17 06:49:23 2010 -0800
@@ -32,6 +32,7 @@
   "Tools/async_manager.ML"
   "Tools/try.ML"
   ("Tools/cnf_funcs.ML")
+  ("Tools/functorial_mappers.ML")
 begin
 
 setup {* Intuitionistic.method_setup @{binding iprover} *}
@@ -708,6 +709,7 @@
   and [Pure.elim?] = iffD1 iffD2 impE
 
 use "Tools/hologic.ML"
+use "Tools/functorial_mappers.ML"
 
 
 subsubsection {* Atomizing meta-level connectives *}
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/IsaMakefile	Wed Nov 17 06:49:23 2010 -0800
@@ -136,6 +136,7 @@
   $(SRC)/Tools/solve_direct.ML \
   $(SRC)/Tools/value.ML \
   HOL.thy \
+  Tools/functorial_mappers.ML \
   Tools/hologic.ML \
   Tools/recfun_codegen.ML \
   Tools/simpdata.ML
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_config.ML	Wed Nov 17 06:49:23 2010 -0800
@@ -25,6 +25,7 @@
   val monomorph_limit: int Config.T
   val drop_bad_facts: bool Config.T
   val filter_only_facts: bool Config.T
+  val debug_files: string Config.T
 
   (*tools*)
   val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
@@ -131,6 +132,10 @@
 val (filter_only_facts, setup_filter_only_facts) =
   Attrib.config_bool filter_only_factsN (K false)
 
+val debug_filesN = "smt_debug_files"
+val (debug_files, setup_debug_files) =
+  Attrib.config_string debug_filesN (K "")
+
 val setup_options =
   setup_oracle #>
   setup_datatypes #>
@@ -141,7 +146,8 @@
   setup_monomorph_limit #>
   setup_drop_bad_facts #>
   setup_filter_only_facts #>
-  setup_trace_used_facts
+  setup_trace_used_facts #>
+  setup_debug_files
 
 
 (* diagnostics *)
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 17 06:49:23 2010 -0800
@@ -162,10 +162,12 @@
     addsimps [@{thm Nat_Numeral.int_nat_number_of}]
     addsimps @{thms neg_simps}
 
+  val int_eq = Thm.cterm_of @{theory} @{const "==" (int)}
+
   fun cancel_int_nat_simproc _ ss ct = 
     let
       val num = Thm.dest_arg (Thm.dest_arg ct)
-      val goal = Thm.mk_binop @{cterm "op == :: int => _"} ct num
+      val goal = Thm.mk_binop int_eq ct num
       val simpset = Simplifier.inherit_context ss cancel_int_nat_ss
       fun tac _ = Simplifier.simp_tac simpset 1
     in on_positive num (Goal.prove_internal [] goal) tac end
@@ -180,8 +182,8 @@
   fun conv ctxt = Simplifier.rewrite (Simplifier.context ctxt nat_ss)
 
   val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat}))
-  val uses_nat_int =
-    Term.exists_subterm (member (op aconv) [@{term int}, @{term nat}])
+  val uses_nat_int = Term.exists_subterm (member (op aconv)
+    [@{const of_nat (int)}, @{const nat}])
 in
 fun nat_as_int ctxt =
   map (apsnd ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt))) #>
@@ -285,7 +287,7 @@
 
 fun norm_def ctxt thm =
   (case Thm.prop_of thm of
-    @{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
+    @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
       norm_def ctxt (thm RS @{thm fun_cong})
   | Const (@{const_name "=="}, _) $ _ $ Abs _ =>
       norm_def ctxt (thm RS @{thm meta_eq_to_obj_eq})
@@ -293,7 +295,7 @@
 
 fun atomize_conv ctxt ct =
   (case Thm.term_of ct of
-    @{term "op ==>"} $ _ $ _ =>
+    @{const "==>"} $ _ $ _ =>
       Conv.binop_conv (atomize_conv ctxt) then_conv
       Conv.rewr_conv @{thm atomize_imp}
   | Const (@{const_name "=="}, _) $ _ $ _ =>
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/Tools/SMT/smt_real.ML
--- a/src/HOL/Tools/SMT/smt_real.ML	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_real.ML	Wed Nov 17 06:49:23 2010 -0800
@@ -63,7 +63,7 @@
 (* Z3 builtins *)
 
 local
-  fun z3_builtin_fun @{term "op / :: real => _"} ts = SOME ("/", ts)
+  fun z3_builtin_fun @{const divide (real)} ts = SOME ("/", ts)
     | z3_builtin_fun _ _ = NONE
 in
 
@@ -86,13 +86,13 @@
     if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
     else NONE
 
-  val mk_uminus = Thm.capply @{cterm "uminus :: real => _"}
-  val mk_add = Thm.mk_binop @{cterm "op + :: real => _"}
-  val mk_sub = Thm.mk_binop @{cterm "op - :: real => _"}
-  val mk_mul = Thm.mk_binop @{cterm "op * :: real => _"}
-  val mk_div = Thm.mk_binop @{cterm "op / :: real => _"}
-  val mk_lt = Thm.mk_binop @{cterm "op < :: real => _"}
-  val mk_le = Thm.mk_binop @{cterm "op <= :: real => _"}
+  val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (real)})
+  val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (real)})
+  val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)})
+  val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)})
+  val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)})
+  val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)})
+  val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)})
 
   fun z3_mk_builtin_fun (I.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
     | z3_mk_builtin_fun (I.Sym ("+", _)) [ct, cu] = SOME (mk_add ct cu)
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Wed Nov 17 06:49:23 2010 -0800
@@ -108,7 +108,17 @@
 
 fun run ctxt cmd args input =
   (case C.certificates_of ctxt of
-    NONE => Cache_IO.run (make_cmd (choose cmd) args) input
+    NONE =>
+      if Config.get ctxt C.debug_files = "" then
+        Cache_IO.run (make_cmd (choose cmd) args) input
+      else
+        let
+          val base_path = Path.explode (Config.get ctxt C.debug_files)
+          val in_path = Path.ext "smt_in" base_path
+          val out_path = Path.ext "smt_out" base_path
+        in
+          Cache_IO.raw_run (make_cmd (choose cmd) args) input in_path out_path 
+        end
   | SOME certs =>
       (case Cache_IO.lookup certs input of
         (NONE, key) =>
@@ -254,6 +264,8 @@
         in
           raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat, ts))
         end)
+
+  val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False})
 in
 
 fun add_solver cfg =
@@ -261,7 +273,7 @@
     val {name, env_var, is_remote, options, interface, outcome, cex_parser,
       reconstruct} = cfg
 
-    fun core_oracle () = @{cprop False}
+    fun core_oracle () = cfalse
 
     fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
       interface=interface,
@@ -302,6 +314,8 @@
       "contains the universal sort {}"))
   else solver_of ctxt rm ctxt irules
 
+val cnot = Thm.cterm_of @{theory} @{const Not}
+
 fun smt_filter run_remote time_limit st xrules i =
   let
     val {facts, goal, ...} = Proof.goal st
@@ -312,10 +326,8 @@
       |> Config.put C.drop_bad_facts true
       |> Config.put C.filter_only_facts true
     val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
-    val cprop =
-      concl
-      |> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt'
-      |> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg
+    fun negate ct = Thm.dest_comb ct ||> Thm.capply cnot |-> Thm.capply
+    val cprop = negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl))
     val irs = map (pair ~1) (Thm.assume cprop :: prems @ facts)
     val rm = SOME run_remote
   in
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Nov 17 06:49:23 2010 -0800
@@ -134,7 +134,7 @@
       | (ps, [false]) => cons (SNoPat ps)
       | _ => raise TERM ("dest_pats", ts))
 
-fun dest_trigger (@{term trigger} $ tl $ t) =
+fun dest_trigger (@{const trigger} $ tl $ t) =
       (rev (fold (dest_pats o HOLogic.dest_list) (HOLogic.dest_list tl) []), t)
   | dest_trigger t = ([], t)
 
@@ -161,8 +161,8 @@
 
 val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn
     Const (@{const_name Let}, _) => true
-  | @{term "op = :: bool => _"} $ _ $ @{term True} => true
-  | Const (@{const_name If}, _) $ _ $ @{term True} $ @{term False} => true
+  | @{const HOL.eq (bool)} $ _ $ @{const True} => true
+  | Const (@{const_name If}, _) $ _ $ @{const True} $ @{const False} => true
   | _ => false)
 
 val rewrite_rules = [
@@ -199,11 +199,11 @@
     fun conn (n, T) = (n, mapTs as_propT as_propT T)
     fun pred (n, T) = (n, mapTs I as_propT T)
 
-    val term_eq = @{term "op = :: bool => _"} |> Term.dest_Const |> pred
-    fun as_term t = Const term_eq $ t $ @{term True}
+    val term_eq = @{const HOL.eq (bool)} |> Term.dest_Const |> pred
+    fun as_term t = Const term_eq $ t $ @{const True}
 
     val if_term = Const (@{const_name If}, [propT, boolT, boolT] ---> boolT)
-    fun wrap_in_if t = if_term $ t $ @{term True} $ @{term False}
+    fun wrap_in_if t = if_term $ t $ @{const True} $ @{const False}
 
     fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
 
@@ -225,7 +225,7 @@
     and in_pats ps =
       in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps
 
-    and in_trig ((c as @{term trigger}) $ p $ t) = c $ in_pats p $ in_form t
+    and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_form t
       | in_trig t = in_form t
 
     and in_form t =
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/Tools/SMT/smt_word.ML
--- a/src/HOL/Tools/SMT/smt_word.ML	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_word.ML	Wed Nov 17 06:49:23 2010 -0800
@@ -60,7 +60,7 @@
 
   fun dest_word_funT (Type ("fun", [T, U])) = (dest_wordT T, dest_wordT U)
     | dest_word_funT T = raise TYPE ("dest_word_funT", [T], [])
-  fun dest_nat (@{term nat} $ n :: ts) = (snd (HOLogic.dest_number n), ts)
+  fun dest_nat (@{const nat} $ n :: ts) = (snd (HOLogic.dest_number n), ts)
     | dest_nat ts = raise TERM ("dest_nat", ts)
   fun dest_nat_word_funT (T, ts) =
     (dest_word_funT (Term.range_type T), dest_nat ts)
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Wed Nov 17 06:49:23 2010 -0800
@@ -70,8 +70,8 @@
   val {is_builtin_pred, ...}= the strict
   val {builtin_typ, builtin_num, builtin_fun, ...} = builtins
 
-  fun is_int_div_mod @{term "op div :: int => _"} = true
-    | is_int_div_mod @{term "op mod :: int => _"} = true
+  fun is_int_div_mod @{const div (int)} = true
+    | is_int_div_mod @{const mod (int)} = true
     | is_int_div_mod _ = false
 
   fun add_div_mod irules =
@@ -170,11 +170,13 @@
 val destT1 = hd o Thm.dest_ctyp
 val destT2 = hd o tl o Thm.dest_ctyp
 
-val mk_true = @{cterm "~False"}
-val mk_false = @{cterm False}
-val mk_not = Thm.capply @{cterm Not}
-val mk_implies = Thm.mk_binop @{cterm HOL.implies}
-val mk_iff = Thm.mk_binop @{cterm "op = :: bool => _"}
+val mk_true = Thm.cterm_of @{theory} (@{const Not} $ @{const False})
+val mk_false = Thm.cterm_of @{theory} @{const False}
+val mk_not = Thm.capply (Thm.cterm_of @{theory} @{const Not})
+val mk_implies = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.implies})
+val mk_iff = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.eq (bool)})
+val conj = Thm.cterm_of @{theory} @{const HOL.conj}
+val disj = Thm.cterm_of @{theory} @{const HOL.disj}
 
 fun mk_nary _ cu [] = cu
   | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
@@ -205,22 +207,22 @@
   let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
   in Thm.capply (Thm.mk_binop (instTs cTs update) array index) value end
 
-val mk_uminus = Thm.capply @{cterm "uminus :: int => _"}
-val mk_add = Thm.mk_binop @{cterm "op + :: int => _"}
-val mk_sub = Thm.mk_binop @{cterm "op - :: int => _"}
-val mk_mul = Thm.mk_binop @{cterm "op * :: int => _"}
-val mk_div = Thm.mk_binop @{cterm "z3div :: int => _"}
-val mk_mod = Thm.mk_binop @{cterm "z3mod :: int => _"}
-val mk_lt = Thm.mk_binop @{cterm "op < :: int => _"}
-val mk_le = Thm.mk_binop @{cterm "op <= :: int => _"}
+val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (int)})
+val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (int)})
+val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (int)})
+val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (int)})
+val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3div})
+val mk_mod = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3mod})
+val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (int)})
+val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (int)})
 
 fun mk_builtin_fun ctxt sym cts =
   (case (sym, cts) of
     (Sym ("true", _), []) => SOME mk_true
   | (Sym ("false", _), []) => SOME mk_false
   | (Sym ("not", _), [ct]) => SOME (mk_not ct)
-  | (Sym ("and", _), _) => SOME (mk_nary @{cterm HOL.conj} mk_true cts)
-  | (Sym ("or", _), _) => SOME (mk_nary @{cterm HOL.disj} mk_false cts)
+  | (Sym ("and", _), _) => SOME (mk_nary conj mk_true cts)
+  | (Sym ("or", _), _) => SOME (mk_nary disj mk_false cts)
   | (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu)
   | (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu)
   | (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu)
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/Tools/SMT/z3_model.ML
--- a/src/HOL/Tools/SMT/z3_model.ML	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/z3_model.ML	Wed Nov 17 06:49:23 2010 -0800
@@ -115,7 +115,7 @@
     fun match ts ((n, _), _) = matches terms (member (op aconv) ts) n
 
     val (default_int, ints) =
-      (case find_first (match [@{term int}]) vs of
+      (case find_first (match [@{const of_nat (int)}]) vs of
         NONE => (NONE, [])
       | SOME (_, cases) =>
           let val (cs, (_, e)) = split_last cases
@@ -138,7 +138,7 @@
       | SOME t => ((n, k), map (subst_nat (Term.fastype_of t) k) cases))
   in
     map subst_nats vs
-    |> filter_out (match [@{term int}, @{term nat}])
+    |> filter_out (match [@{const of_nat (int)}, @{const nat}])
   end
 
 fun filter_valid_valuations terms = map_filter (fn
@@ -179,8 +179,8 @@
 
 fun get_term n (cx as (_, terms, _)) = (the (Symtab.lookup terms n), cx)
 
-fun trans_expr _ True = pair @{term True}
-  | trans_expr _ False = pair @{term False}
+fun trans_expr _ True = pair @{const True}
+  | trans_expr _ False = pair @{const False}
   | trans_expr T (Number (i, NONE)) = pair (HOLogic.mk_number T i)
   | trans_expr T (Number (i, SOME j)) =
       pair (Const (@{const_name divide}, [T, T] ---> T) $
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/Tools/SMT/z3_proof_literals.ML
--- a/src/HOL/Tools/SMT/z3_proof_literals.ML	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/z3_proof_literals.ML	Wed Nov 17 06:49:23 2010 -0800
@@ -22,6 +22,7 @@
   val is_conj: term -> bool
   val is_disj: term -> bool
   val exists_lit: bool -> (term -> bool) -> term -> bool
+  val negate: cterm -> cterm
 
   (* proof tools *)
   val explode: bool -> bool -> bool -> term list -> thm -> thm list
@@ -59,19 +60,19 @@
 
 (** properties and term operations **)
 
-val is_neg = (fn @{term Not} $ _ => true | _ => false)
-fun is_neg' f = (fn @{term Not} $ t => f t | _ => false)
+val is_neg = (fn @{const Not} $ _ => true | _ => false)
+fun is_neg' f = (fn @{const Not} $ t => f t | _ => false)
 val is_dneg = is_neg' is_neg
-val is_conj = (fn @{term HOL.conj} $ _ $ _ => true | _ => false)
-val is_disj = (fn @{term HOL.disj} $ _ $ _ => true | _ => false)
+val is_conj = (fn @{const HOL.conj} $ _ $ _ => true | _ => false)
+val is_disj = (fn @{const HOL.disj} $ _ $ _ => true | _ => false)
 
 fun dest_disj_term' f = (fn
-    @{term Not} $ (@{term HOL.disj} $ t $ u) => SOME (f t, f u)
+    @{const Not} $ (@{const HOL.disj} $ t $ u) => SOME (f t, f u)
   | _ => NONE)
 
-val dest_conj_term = (fn @{term HOL.conj} $ t $ u => SOME (t, u) | _ => NONE)
+val dest_conj_term = (fn @{const HOL.conj} $ t $ u => SOME (t, u) | _ => NONE)
 val dest_disj_term =
-  dest_disj_term' (fn @{term Not} $ t => t | t => @{term Not} $ t)
+  dest_disj_term' (fn @{const Not} $ t => t | t => @{const Not} $ t)
 
 fun exists_lit is_conj P =
   let
@@ -82,6 +83,8 @@
       | NONE => false)
   in exists end
 
+val negate = Thm.capply (Thm.cterm_of @{theory} @{const Not})
+
 
 
 (** proof tools **)
@@ -135,7 +138,7 @@
           end
       | NONE => add (t, rev rules))
 
-    fun explode0 (@{term Not} $ (@{term Not} $ t)) =
+    fun explode0 (@{const Not} $ (@{const Not} $ t)) =
           Termtab.make [(t, [dneg_rule])]
       | explode0 t = explode1 [] t Termtab.empty
 
@@ -202,23 +205,23 @@
     | comp_disj ((true, thm1), (false, thm2)) = comp2 disj3 thm1 thm2
     | comp_disj ((true, thm1), (true, thm2)) = comp2 disj4 thm1 thm2
 
-  fun dest_conj (@{term HOL.conj} $ t $ u) = ((false, t), (false, u))
+  fun dest_conj (@{const HOL.conj} $ t $ u) = ((false, t), (false, u))
     | dest_conj t = raise TERM ("dest_conj", [t])
 
-  val neg = (fn @{term Not} $ t => (true, t) | t => (false, @{term Not} $ t))
-  fun dest_disj (@{term Not} $ (@{term HOL.disj} $ t $ u)) = (neg t, neg u)
+  val neg = (fn @{const Not} $ t => (true, t) | t => (false, @{const Not} $ t))
+  fun dest_disj (@{const Not} $ (@{const HOL.disj} $ t $ u)) = (neg t, neg u)
     | dest_disj t = raise TERM ("dest_disj", [t])
 
   val dnegE = T.precompose (single o d2 o d1) @{thm notnotD}
   val dnegI = T.precompose (single o d1) @{lemma "P ==> ~~P" by fast}
-  fun as_dneg f t = f (@{term Not} $ (@{term Not} $ t))
+  fun as_dneg f t = f (@{const Not} $ (@{const Not} $ t))
 
   fun dni f = apsnd f o Thm.dest_binop o f o d1
   val negIffE = T.precompose2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast}
   val negIffI = T.precompose2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast}
-  val iff_const = @{term "op = :: bool => _"}
-  fun as_negIff f (@{term "op = :: bool => _"} $ t $ u) =
-        f (@{term Not} $ (iff_const $ u $ (@{term Not} $ t)))
+  val iff_const = @{const HOL.eq (bool)}
+  fun as_negIff f (@{const HOL.eq (bool)} $ t $ u) =
+        f (@{const Not} $ (iff_const $ u $ (@{const Not} $ t)))
     | as_negIff _ _ = NONE
 in
 
@@ -231,12 +234,12 @@
 
     fun lookup_rule t =
       (case t of
-        @{term Not} $ (@{term Not} $ t) => (T.compose dnegI, lookup t)
-      | @{term Not} $ (@{term "op = :: bool => _"} $ t $ (@{term Not} $ u)) =>
-          (T.compose negIffI, lookup (iff_const $ u $ t))
-      | @{term Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
+        @{const Not} $ (@{const Not} $ t) => (T.compose dnegI, lookup t)
+      | @{const Not} $ (@{const HOL.eq (bool)} $ t $ (@{const Not} $ u)) =>
+            (T.compose negIffI, lookup (iff_const $ u $ t))
+      | @{const Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
           let fun rewr lit = lit COMP @{thm not_sym}
-          in (rewr, lookup (@{term Not} $ (eq $ u $ t))) end
+          in (rewr, lookup (@{const Not} $ (eq $ u $ t))) end
       | _ =>
           (case as_dneg lookup t of
             NONE => (T.compose negIffE, as_negIff lookup t)
@@ -264,11 +267,10 @@
   val cp1 = @{lemma "(~P) = (~Q) ==> P = Q" by simp}
   val cp2 = @{lemma "(~P) = Q ==> P = (~Q)" by fastsimp}
   val cp3 = @{lemma "P = (~Q) ==> (~P) = Q" by simp}
-  val neg = Thm.capply @{cterm Not}
 in
-fun contrapos1 prove (ct, cu) = prove (neg ct, neg cu) COMP cp1
-fun contrapos2 prove (ct, cu) = prove (neg ct, Thm.dest_arg cu) COMP cp2
-fun contrapos3 prove (ct, cu) = prove (Thm.dest_arg ct, neg cu) COMP cp3
+fun contrapos1 prove (ct, cu) = prove (negate ct, negate cu) COMP cp1
+fun contrapos2 prove (ct, cu) = prove (negate ct, Thm.dest_arg cu) COMP cp2
+fun contrapos3 prove (ct, cu) = prove (Thm.dest_arg ct, negate cu) COMP cp3
 end
 
 
@@ -279,10 +281,10 @@
       val rules = explode_term conj (T.prop_of thm)
       fun contra_lits (t, rs) =
         (case t of
-          @{term Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
+          @{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
         | _ => NONE)
     in
-      (case Termtab.lookup rules @{term False} of
+      (case Termtab.lookup rules @{const False} of
         SOME rs => extract_lit thm rs
       | NONE =>
           the (Termtab.get_first contra_lits rules)
@@ -322,8 +324,9 @@
   let val cp as (cl, cr) = Thm.dest_binop (Thm.dest_arg ct)
   in
     (case (kind_of (Thm.term_of cl), Thm.term_of cr) of
-      (SOME CONJ, @{term False}) => contradict true cl
-    | (SOME DISJ, @{term "~False"}) => contrapos2 (contradict false o fst) cp
+      (SOME CONJ, @{const False}) => contradict true cl
+    | (SOME DISJ, @{const Not} $ @{const False}) =>
+        contrapos2 (contradict false o fst) cp
     | (kl, _) =>
         (case (kl, kind_of (Thm.term_of cr)) of
           (SOME CONJ, SOME CONJ) => prove_eq true true cp
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/Tools/SMT/z3_proof_parser.ML
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Wed Nov 17 06:49:23 2010 -0800
@@ -113,10 +113,11 @@
     fun mk (i, v) = (v, certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
   in map mk vars end
 
+val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
+
 fun close ctxt (ct, vars) =
   let
     val inst = mk_inst ctxt vars
-    val mk_prop = Thm.capply @{cterm Trueprop}
     val names = fold (Term.add_free_names o Thm.term_of o snd) inst []
   in (mk_prop (Thm.instantiate_cterm ([], inst) ct), names) end
 
@@ -182,6 +183,8 @@
 
 (* parser context *)
 
+val not_false = Thm.cterm_of @{theory} (@{const Not} $ @{const False})
+
 fun make_context ctxt typs terms =
   let
     val ctxt' = 
@@ -189,7 +192,7 @@
       |> Symtab.fold (Variable.declare_typ o snd) typs
       |> Symtab.fold (Variable.declare_term o snd) terms
 
-    fun cert @{term True} = @{cterm "~False"}
+    fun cert @{const True} = not_false
       | cert t = certify ctxt' t
 
   in (typs, Symtab.map (K cert) terms, Inttab.empty, Inttab.empty, [], ctxt') end
@@ -357,8 +360,10 @@
 
 fun pats st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st
 
+val ctrue = Thm.cterm_of @{theory} @{const True}
+
 fun pattern st = par (this "pattern" |-- Scan.repeat1 (sep arg) >>
-  (the o mk_fun (K (SOME @{cterm True})))) st
+  (the o mk_fun (K (SOME ctrue)))) st
 
 fun quant_kind st = st |> (
   this "forall" >> K (mk_forall o theory_of) ||
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Nov 17 06:49:23 2010 -0800
@@ -231,7 +231,7 @@
 in
 fun lemma thm ct =
   let
-    val cu = Thm.capply @{cterm Not} (Thm.dest_arg ct)
+    val cu = L.negate (Thm.dest_arg ct)
     val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
   in Thm (T.compose ccontr (T.under_assumption (intro hyps thm) cu)) end
 end
@@ -243,7 +243,7 @@
   val explode_disj = L.explode false true false
   val join_disj = L.join false
   fun unit thm thms th =
-    let val t = @{term Not} $ T.prop_of thm and ts = map T.prop_of thms
+    let val t = @{const Not} $ T.prop_of thm and ts = map T.prop_of thms
     in join_disj (L.make_littab (thms @ explode_disj ts th)) t end
 
   fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
@@ -251,7 +251,7 @@
   val contrapos = T.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
 in
 fun unit_resolution thm thms ct =
-  Thm.capply @{cterm Not} (Thm.dest_arg ct)
+  L.negate (Thm.dest_arg ct)
   |> T.under_assumption (unit thm thms)
   |> Thm o T.discharge thm o T.compose contrapos
 end
@@ -295,14 +295,14 @@
     let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
     in
       (case Thm.term_of ct1 of
-        @{term Not} $ (@{term HOL.conj} $ _ $ _) =>
+        @{const Not} $ (@{const HOL.conj} $ _ $ _) =>
           prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
-      | @{term HOL.conj} $ _ $ _ =>
-          prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, true)
-      | @{term Not} $ (@{term HOL.disj} $ _ $ _) =>
-          prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, false)
-      | @{term HOL.disj} $ _ $ _ =>
-          prove disjI2 (Thm.capply @{cterm Not} ct1, false) (ct2, true)
+      | @{const HOL.conj} $ _ $ _ =>
+          prove disjI3 (L.negate ct2, false) (ct1, true)
+      | @{const Not} $ (@{const HOL.disj} $ _ $ _) =>
+          prove disjI3 (L.negate ct2, false) (ct1, false)
+      | @{const HOL.disj} $ _ $ _ =>
+          prove disjI2 (L.negate ct1, false) (ct2, true)
       | Const (@{const_name SMT.distinct}, _) $ _ =>
           let
             fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
@@ -310,7 +310,7 @@
               let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
               in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
           in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end
-      | @{term Not} $ (Const (@{const_name SMT.distinct}, _) $ _) =>
+      | @{const Not} $ (Const (@{const_name SMT.distinct}, _) $ _) =>
           let
             fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
             fun prv cu =
@@ -392,7 +392,7 @@
       if l aconv r
       then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
       else MetaEq (nnf_quant vars quant_rules1 (hd ps) ct)
-  | _ $ (@{term Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
+  | _ $ (@{const Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
       MetaEq (nnf_quant vars quant_rules2 (hd ps) ct)
   | _ =>
       let
@@ -474,8 +474,8 @@
 
   fun mono f (cp as (cl, _)) =
     (case Term.head_of (Thm.term_of cl) of
-      @{term HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
-    | @{term HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
+      @{const HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
+    | @{const HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
     | Const (@{const_name SMT.distinct}, _) => prove_distinct (prove_eq_safe f)
     | _ => prove (prove_eq_safe f)) cp
 in
@@ -589,8 +589,8 @@
     |> Conv.fconv_rule (Thm.beta_conversion true)
 
   fun kind (Const (@{const_name Ex}, _) $ _) = (sk_ex_rule, I, I)
-    | kind (@{term Not} $ (Const (@{const_name All}, _) $ _)) =
-        (sk_all_rule, Thm.dest_arg, Thm.capply @{cterm Not})
+    | kind (@{const Not} $ (Const (@{const_name All}, _) $ _)) =
+        (sk_all_rule, Thm.dest_arg, L.negate)
     | kind t = raise TERM ("skolemize", [t])
 
   fun dest_abs_type (Abs (_, T, _)) = T
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/Tools/SMT/z3_proof_tools.ML
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Nov 17 06:49:23 2010 -0800
@@ -53,12 +53,12 @@
 
 (* accessing terms *)
 
-val dest_prop = (fn @{term Trueprop} $ t => t | t => t)
+val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
 
 fun term_of ct = dest_prop (Thm.term_of ct)
 fun prop_of thm = dest_prop (Thm.prop_of thm)
 
-val mk_prop = Thm.capply @{cterm Trueprop}
+val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
 
 val eq = I.mk_inst_pair I.destT1 @{cpat "op =="}
 fun mk_meta_eq_cterm ct cu = Thm.mk_binop (I.instT' ct eq) ct cu
@@ -195,14 +195,14 @@
 
     and abstr cvs ct =
       (case Thm.term_of ct of
-        @{term Trueprop} $ _ => abstr1 cvs ct
-      | @{term "op ==>"} $ _ $ _ => abstr2 cvs ct
-      | @{term True} => pair ct
-      | @{term False} => pair ct
-      | @{term Not} $ _ => abstr1 cvs ct
-      | @{term HOL.conj} $ _ $ _ => abstr2 cvs ct
-      | @{term HOL.disj} $ _ $ _ => abstr2 cvs ct
-      | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
+        @{const Trueprop} $ _ => abstr1 cvs ct
+      | @{const "==>"} $ _ $ _ => abstr2 cvs ct
+      | @{const True} => pair ct
+      | @{const False} => pair ct
+      | @{const Not} $ _ => abstr1 cvs ct
+      | @{const HOL.conj} $ _ $ _ => abstr2 cvs ct
+      | @{const HOL.disj} $ _ $ _ => abstr2 cvs ct
+      | @{const HOL.implies} $ _ $ _ => abstr2 cvs ct
       | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct
       | Const (@{const_name SMT.distinct}, _) $ _ =>
           if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
@@ -221,8 +221,10 @@
           else fresh_abstraction cvs ct cx))
   in abstr [] end
 
+val cimp = Thm.cterm_of @{theory} @{const "==>"}
+
 fun with_prems thms f ct =
-  fold_rev (Thm.mk_binop @{cterm "op ==>"} o Thm.cprop_of) thms ct
+  fold_rev (Thm.mk_binop cimp o Thm.cprop_of) thms ct
   |> f
   |> fold (fn prem => fn th => Thm.implies_elim th prem) thms
 
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/HOL/Tools/functorial_mappers.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/functorial_mappers.ML	Wed Nov 17 06:49:23 2010 -0800
@@ -0,0 +1,210 @@
+(*  Title:      HOL/Tools/functorial_mappers.ML
+    Author:     Florian Haftmann, TU Muenchen
+
+Functorial mappers on types.
+*)
+
+signature FUNCTORIAL_MAPPERS =
+sig
+  val find_atomic: theory -> typ -> (typ * (bool * bool)) list
+  val construct_mapper: theory -> (string * bool -> term)
+    -> bool -> typ -> typ -> term
+  val register: string -> string -> (sort * (bool * bool)) list -> thm -> thm
+    -> theory -> theory
+  val type_mapper: term -> theory -> Proof.state
+  type entry
+  val entries: theory -> entry Symtab.table
+end;
+
+structure Functorial_Mappers : FUNCTORIAL_MAPPERS =
+struct
+
+(** functorial mappers and their properties **)
+
+(* bookkeeping *)
+
+type entry = { mapper: string, variances: (sort * (bool * bool)) list,
+  concatenate: thm, identity: thm };
+
+structure Data = Theory_Data(
+  type T = entry Symtab.table
+  val empty = Symtab.empty
+  val merge = Symtab.merge (K true)
+  val extend = I
+);
+
+val entries = Data.get;
+
+
+(* type analysis *)
+
+fun find_atomic thy T =
+  let
+    val variances_of = Option.map #variances o Symtab.lookup (Data.get thy);
+    fun add_variance is_contra T =
+      AList.map_default (op =) (T, (false, false))
+        ((if is_contra then apsnd else apfst) (K true));
+    fun analyze' is_contra (_, (co, contra)) T =
+      (if co then analyze is_contra T else I)
+      #> (if contra then analyze (not is_contra) T else I)
+    and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco
+          of NONE => add_variance is_contra T
+           | SOME variances => fold2 (analyze' is_contra) variances Ts)
+      | analyze is_contra T = add_variance is_contra T;
+  in analyze false T [] end;
+
+fun construct_mapper thy atomic =
+  let
+    val lookup = the o Symtab.lookup (Data.get thy);
+    fun constructs is_contra (_, (co, contra)) T T' =
+      (if co then [construct is_contra T T'] else [])
+      @ (if contra then [construct (not is_contra) T T'] else [])
+    and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) =
+          let
+            val { mapper, variances, ... } = lookup tyco;
+            val args = maps (fn (arg_pattern, (T, T')) =>
+              constructs is_contra arg_pattern T T')
+                (variances ~~ (Ts ~~ Ts'));
+            val (U, U') = if is_contra then (T', T) else (T, T');
+          in list_comb (Const (mapper, map fastype_of args ---> U --> U'), args) end
+      | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra);
+  in construct end;
+
+
+(* mapper properties *)
+
+fun make_concatenate_prop variances (tyco, mapper) =
+  let
+    fun invents n k nctxt =
+      let
+        val names = Name.invents nctxt n k;
+      in (names, fold Name.declare names nctxt) end;
+    val (((vs1, vs2), vs3), _) = Name.context
+      |> invents Name.aT (length variances)
+      ||>> invents Name.aT (length variances)
+      ||>> invents Name.aT (length variances);
+    fun mk_Ts vs = map2 (fn v => fn (sort, _) => TFree (v, sort))
+      vs variances;
+    val (Ts1, Ts2, Ts3) = (mk_Ts vs1, mk_Ts vs2, mk_Ts vs3);
+    fun mk_argT ((T, T'), (_, (co, contra))) =
+      (if co then [(T --> T')] else [])
+      @ (if contra then [(T' --> T)] else []);
+    val contras = maps (fn (_, (co, contra)) =>
+      (if co then [false] else []) @ (if contra then [true] else [])) variances;
+    val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances);
+    val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
+    val ((names21, names32), nctxt) = Name.context
+      |> invents "f" (length Ts21)
+      ||>> invents "f" (length Ts32);
+    val T1 = Type (tyco, Ts1);
+    val T2 = Type (tyco, Ts2);
+    val T3 = Type (tyco, Ts3);
+    val x = Free (the_single (Name.invents nctxt "a" 1), T3);
+    val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32);
+    val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) =>
+      if not is_contra then
+        Abs ("x", domain_type T32, Free (f21, T21) $ (Free (f32, T32) $ Bound 0))
+      else
+        Abs ("x", domain_type T21, Free (f32, T32) $ (Free (f21, T21) $ Bound 0))
+      ) contras (args21 ~~ args32)
+    fun mk_mapper T T' args = list_comb (Const (mapper,
+      map fastype_of args ---> T --> T'), args);
+    val lhs = mk_mapper T2 T1 (map Free args21) $
+      (mk_mapper T3 T2 (map Free args32) $ x);
+    val rhs = mk_mapper T3 T1 args31 $ x;
+  in (x, (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, rhs)) end;
+
+fun make_identity_prop variances (tyco, mapper) =
+  let
+    val vs = Name.invents Name.context Name.aT (length variances);
+    val Ts = map2 (fn v => fn (sort, _) => TFree (v, sort)) vs variances;
+    fun bool_num b = if b then 1 else 0;
+    fun mk_argT (T, (_, (co, contra))) =
+      replicate (bool_num co + bool_num contra) (T --> T)
+    val Ts' = maps mk_argT (Ts ~~ variances)
+    val T = Type (tyco, Ts);
+    val x = Free ("a", T);
+    val lhs = list_comb (Const (mapper, Ts' ---> T --> T),
+      map (fn T => Abs ("x", domain_type T, Bound 0)) Ts') $ x;
+  in (x, (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, x)) end;
+
+
+(* registering mappers *)
+
+fun register tyco mapper variances raw_concatenate raw_identity thy =
+  let
+    val (_, concatenate_prop) = make_concatenate_prop variances (tyco, mapper);
+    val (_, identity_prop) = make_identity_prop variances (tyco, mapper);
+    val concatenate = Goal.prove_global thy
+      (Term.add_free_names concatenate_prop []) [] concatenate_prop
+      (K (ALLGOALS (ProofContext.fact_tac [raw_concatenate])));
+    val identity = Goal.prove_global thy
+      (Term.add_free_names identity_prop []) [] identity_prop
+      (K (ALLGOALS (ProofContext.fact_tac [raw_identity])));
+  in
+    thy
+    |> Data.map (Symtab.update (tyco, { mapper = mapper,
+        variances = variances,
+        concatenate = concatenate, identity = identity }))
+  end;
+
+fun split_mapper_typ "fun" T =
+      let
+        val (Ts', T') = strip_type T;
+        val (Ts'', T'') = split_last Ts';
+        val (Ts''', T''') = split_last Ts'';
+      in (Ts''', T''', T'' --> T') end
+  | split_mapper_typ tyco T =
+      let
+        val (Ts', T') = strip_type T;
+        val (Ts'', T'') = split_last Ts';
+      in (Ts'', T'', T') end;
+
+fun analyze_variances thy tyco T =
+  let
+    fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ_global thy T);
+    val (Ts, T1, T2) = split_mapper_typ tyco T
+      handle List.Empty => bad_typ ();
+    val _ = pairself
+      ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
+    val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2)
+      handle TYPE _ => bad_typ ();
+    val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
+      then bad_typ () else ();
+  in [] end;
+
+fun gen_type_mapper prep_term raw_t thy =
+  let
+    val (mapper, T) = case prep_term thy raw_t
+     of Const cT => cT
+      | t => error ("No constant: " ^ Syntax.string_of_term_global thy t);
+    val _ = Type.no_tvars T;
+    fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
+      | add_tycos _ = I;
+    val tycos = add_tycos T [];
+    val tyco = if tycos = ["fun"] then "fun"
+      else case remove (op =) "fun" tycos
+       of [tyco] => tyco
+        | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T);
+    val variances = analyze_variances thy tyco T;
+    val (_, concatenate_prop) = make_concatenate_prop variances (tyco, mapper);
+    val (_, identity_prop) = make_identity_prop variances (tyco, mapper);
+    fun after_qed [[concatenate], [identity]] lthy =
+      lthy
+      |> (Local_Theory.background_theory o Data.map)
+          (Symtab.update (tyco, { mapper = mapper, variances = variances,
+            concatenate = concatenate, identity = identity }));
+  in
+    thy
+    |> Named_Target.theory_init
+    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [concatenate_prop, identity_prop])
+  end
+
+val type_mapper = gen_type_mapper Sign.cert_term;
+val type_mapper_cmd = gen_type_mapper Syntax.read_term_global;
+
+val _ =
+  Outer_Syntax.command "type_mapper" "register functorial mapper for type with its properties" Keyword.thy_goal
+    (Parse.term >> (fn t => Toplevel.print o (Toplevel.theory_to_proof (type_mapper_cmd t))));
+
+end;
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/Pure/PIDE/command.scala	Wed Nov 17 06:49:23 2010 -0800
@@ -54,7 +54,9 @@
                 val props = Position.purge(atts)
                 val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
                 state.add_markup(info)
-              case _ => System.err.println("Ignored report message: " + msg); state
+              case _ =>
+                // FIXME System.err.println("Ignored report message: " + msg)
+                state
             })
         case XML.Elem(Markup(name, atts), body) =>
           atts match {
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/Pure/System/gui_setup.scala
--- a/src/Pure/System/gui_setup.scala	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/Pure/System/gui_setup.scala	Wed Nov 17 06:49:23 2010 -0800
@@ -39,6 +39,7 @@
     // values
     if (Platform.is_windows)
       text.append("Cygwin root: " + Cygwin.check_root() + "\n")
+    text.append("JVM name: " + System.getProperty("java.vm.name") + "\n")
     text.append("JVM platform: " + Platform.jvm_platform + "\n")
     try {
       val isabelle_system = new Isabelle_System
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/Tools/cache_io.ML	Wed Nov 17 06:49:23 2010 -0800
@@ -13,6 +13,8 @@
     output: string list,
     redirected_output: string list,
     return_code: int}
+  val raw_run: (Path.T -> Path.T -> string) -> string -> Path.T -> Path.T ->
+    result
   val run: (Path.T -> Path.T -> string) -> string -> result
 
   (*cache*)
@@ -52,14 +54,16 @@
   redirected_output: string list,
   return_code: int}
 
+fun raw_run make_cmd str in_path out_path =
+  let
+    val _ = File.write in_path str
+    val (out2, rc) = bash_output (make_cmd in_path out_path)
+    val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
+  in {output=split_lines out2, redirected_output=out1, return_code=rc} end
+
 fun run make_cmd str =
   with_tmp_file cache_io_prefix (fn in_path =>
-  with_tmp_file cache_io_prefix (fn out_path =>
-    let
-      val _ = File.write in_path str
-      val (out2, rc) = bash_output (make_cmd in_path out_path)
-      val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
-    in {output=split_lines out2, redirected_output=out1, return_code=rc} end))
+  with_tmp_file cache_io_prefix (raw_run make_cmd str in_path))
 
 
 (* cache *)
diff -r b994d855dbd2 -r 1c0b5bfa52a1 src/Tools/jEdit/dist-template/lib/Tools/jedit
--- a/src/Tools/jEdit/dist-template/lib/Tools/jedit	Tue Nov 16 16:36:57 2010 -0800
+++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit	Wed Nov 17 06:49:23 2010 -0800
@@ -24,7 +24,6 @@
   echo "    -m MODE      add print mode for output"
   echo
   echo "Start jEdit with Isabelle plugin setup and opens theory FILES"
-  echo "(default ~/Scratch.thy)."
   echo
   exit 1
 }
@@ -93,14 +92,10 @@
 
 # args
 
-if [ "$#" -eq 0 ]; then
-  ARGS["${#ARGS[@]}"]="Scratch.thy"
-else
-  while [ "$#" -gt 0 ]; do
-    ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
-    shift
-  done
-fi
+while [ "$#" -gt 0 ]; do
+  ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
+  shift
+done
 
 
 ## default perspective