# HG changeset patch
# User blanchet
# Date 1477694372 -7200
# Node ID 582f54f6b29bd06bca6727d26b9b8bb9e481a445
# Parent  de00179d2147ea2b1c09e3caac4a66e3c3ad651d
adapted Nunchaku integration to keyword renaming

diff -r de00179d2147 -r 582f54f6b29b src/HOL/Nunchaku/Tools/nunchaku_problem.ML
--- a/src/HOL/Nunchaku/Tools/nunchaku_problem.ML	Fri Oct 28 20:41:18 2016 +0200
+++ b/src/HOL/Nunchaku/Tools/nunchaku_problem.ML	Sat Oct 29 00:39:32 2016 +0200
@@ -107,6 +107,7 @@
   val nun_match: string
   val nun_mu: string
   val nun_not: string
+  val nun_partial_quotient: string
   val nun_pred: string
   val nun_prop: string
   val nun_quotient: string
@@ -280,6 +281,7 @@
 val nun_match = "match";
 val nun_mu = "mu";
 val nun_not = "~";
+val nun_partial_quotient = "partial_quotient";
 val nun_pred = "pred";
 val nun_prop = "prop";
 val nun_quotient = "quotient";
@@ -737,9 +739,10 @@
   (case subset of
     NONE => ""
   | SOME s => if is_triv_subset s then "" else "\n  " ^ nun_subset ^ " " ^ str_of_tm s) ^
+  (* TODO: use nun_quotient when possible *)
   (case quotient of
     NONE => ""
-  | SOME q => "\n  " ^ nun_quotient ^ " " ^ str_of_tm q) ^
+  | SOME q => "\n  " ^ nun_partial_quotient ^ " " ^ str_of_tm q) ^
   "\n  " ^ nun_abstract ^ " " ^ str_of_tm abs ^ "\n  " ^ nun_concrete ^ " " ^ str_of_tm rep;
 
 fun str_of_nun_ctr_spec {ctr, arg_tys} =
diff -r de00179d2147 -r 582f54f6b29b src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Fri Oct 28 20:41:18 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Sat Oct 29 00:39:32 2016 +0200
@@ -2,14 +2,16 @@
     Author:     Steffen Juilf Smolka, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
 
-Supplements term with a locally minmal, complete set of type constraints. Complete: The constraints
-suffice to infer the term's types. Minimal: Reducing the set of constraints further will make it
-incomplete.
+Supplements term with a locally minimal, complete set of type constraints.
+Complete: The constraints suffice to infer the term's types. Minimal: Reducing
+the set of constraints further will make it incomplete.
 
-When configuring the pretty printer appropriately, the constraints will show up as type annotations
-when printing the term. This allows the term to be printed and reparsed without a change of types.
+When configuring the pretty printer appropriately, the constraints will show up
+as type annotations when printing the term. This allows the term to be printed
+and reparsed without a change of types.
 
-Note: Terms should be unchecked before calling "annotate_types_in_term" to avoid awkward syntax.
+Terms should be unchecked before calling "annotate_types_in_term" to avoid
+awkward syntax.
 *)
 
 signature SLEDGEHAMMER_ISAR_ANNOTATE =