# HG changeset patch
# User blanchet
# Date 1379954402 -7200
# Node ID de4653037e0d1e29e92e2cfde1b6ccf6f3a544e8
# Parent  4163160853fde047027a87d56e9faf4e8694af46
don't generalize w.r.t. wrong context -- better overgeneralize (since the instantiation phase will compensate for it)

diff -r 4163160853fd -r de4653037e0d src/HOL/BNF/Examples/Stream.thy
--- a/src/HOL/BNF/Examples/Stream.thy	Mon Sep 23 17:43:23 2013 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy	Mon Sep 23 18:40:02 2013 +0200
@@ -17,19 +17,7 @@
 
 declaration {*
   Nitpick_HOL.register_codatatype
-    @{typ "'stream_element_type stream"} @{const_name stream_case} [dest_Const @{term Stream}]
-    (*FIXME: long type variable name required to reduce the probability of
-        a name clash of Nitpick in context. E.g.:
-        context
-        fixes x :: 'stream_element_type
-        begin
-
-        lemma "sset s = {}"
-        nitpick
-        oops
-
-        end
-    *)
+    @{typ "'a stream"} @{const_name stream_case} [dest_Const @{term Stream}]
 *}
 
 code_datatype Stream
diff -r 4163160853fd -r de4653037e0d src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Sep 23 17:43:23 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Sep 23 18:40:02 2013 +0200
@@ -595,8 +595,8 @@
                  @{type_name int}, @{type_name natural}, @{type_name integer}] s orelse
   (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
 
-fun repair_constr_type ctxt body_T' T =
-  varify_and_instantiate_type ctxt (body_type T) body_T' T
+fun repair_constr_type thy body_T' T =
+  varify_and_instantiate_type_global thy (body_type T) body_T' T
 
 fun register_frac_type_generic frac_s ersaetze generic =
   let
@@ -632,7 +632,7 @@
     val ctxt = Context.proof_of generic
     val thy = Context.theory_of generic
     val {frac_types, ersatz_table, codatatypes} = Data.get generic
-    val constr_xs = map (apsnd (repair_constr_type ctxt co_T)) constr_xs
+    val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
     val (co_s, co_Ts) = dest_Type co_T
     val _ =
       if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso
@@ -783,13 +783,15 @@
     raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
 
 fun is_coconstr ctxt (s, T) =
-  case body_type T of
-    co_T as Type (co_s, _) =>
-    let val {codatatypes, ...} = Data.get (Context.Proof ctxt) in
-      exists (fn (s', T') => s = s' andalso repair_constr_type ctxt co_T T' = T)
-             (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these)
-    end
-  | _ => false
+  let val thy = Proof_Context.theory_of ctxt in
+    case body_type T of
+      co_T as Type (co_s, _) =>
+      let val {codatatypes, ...} = Data.get (Context.Proof ctxt) in
+        exists (fn (s', T') => s = s' andalso repair_constr_type thy co_T T' = T)
+               (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these)
+      end
+    | _ => false
+  end
 fun is_constr_like ctxt (s, T) =
   member (op =) [@{const_name FunBox}, @{const_name PairBox},
                  @{const_name Quot}, @{const_name Zero_Rep},
@@ -923,7 +925,7 @@
                               (T as Type (s, Ts)) =
     (case AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt)))
                        s of
-       SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type ctxt T)) xs'
+       SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
      | _ =>
        if is_frac_type ctxt T then
          case typedef_info ctxt s of
diff -r 4163160853fd -r de4653037e0d src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Sep 23 17:43:23 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Sep 23 18:40:02 2013 +0200
@@ -66,6 +66,7 @@
   val varify_type : Proof.context -> typ -> typ
   val instantiate_type : theory -> typ -> typ -> typ -> typ
   val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
+  val varify_and_instantiate_type_global : theory -> typ -> typ -> typ -> typ
   val is_of_class_const : theory -> string * typ -> bool
   val get_class_def : theory -> string -> (string * term) option
   val monomorphic_term : Type.tyenv -> term -> term
@@ -282,6 +283,9 @@
 val instantiate_type = ATP_Util.instantiate_type
 val varify_and_instantiate_type = ATP_Util.varify_and_instantiate_type
 
+fun varify_and_instantiate_type_global thy T1 T1' T2 =
+  instantiate_type thy (Logic.varifyT_global T1) T1' (Logic.varifyT_global T2)
+
 fun is_of_class_const thy (s, _) =
   member (op =) (map Logic.const_of_class (Sign.all_classes thy)) s