src/HOL/Tools/type_lifting.ML

 
 (** functorial mappers and their properties **)
 
 (* bookkeeping *)
 
-fun term_with_typ ctxt T t = Envir.subst_term_types
-  (Type.typ_match (ProofContext.tsig_of ctxt) (fastype_of t, T) Vartab.empty) t;
-
 type entry = { mapper: term, variances: (sort * (bool * bool)) list,
   comp: thm, id: thm };
 
 structure Data = Generic_Data(
   type T = entry Symtab.table

 
 val entries = Data.get o Context.Proof;
 
 
 (* type analysis *)
+
+fun term_with_typ ctxt T t = Envir.subst_term_types
+  (Type.typ_match (ProofContext.tsig_of ctxt) (fastype_of t, T) Vartab.empty) t;
 
 fun find_atomic ctxt T =
   let
     val variances_of = Option.map #variances o Symtab.lookup (entries ctxt);
     fun add_variance is_contra T =

       end;
     val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts;
     val _ = if null left_variances then () else bad_typ ();
   in variances end;
 
-fun gen_type_lifting prep_term some_prfx raw_t thy =
-  let
-    val mapper_fixT = prep_term thy raw_t;
-    val T = fastype_of mapper_fixT;
+fun gen_type_lifting prep_term some_prfx raw_mapper thy =
+  let
+    val input_mapper = prep_term thy raw_mapper;
+    val T = fastype_of input_mapper;
     val _ = Type.no_tvars T;
-    val mapper = singleton (Variable.polymorphic (ProofContext.init_global thy)) mapper_fixT;
+    val mapper = singleton (Variable.polymorphic (ProofContext.init_global thy)) input_mapper;
     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

     val prfx = the_default (Long_Name.base_name tyco) some_prfx;
     val variances = analyze_variances thy tyco T;
     val ctxt = ProofContext.init_global thy;
     val (comp_prop, prove_compositionality) = make_comp_prop ctxt variances (tyco, mapper);
     val (id_prop, prove_identity) = make_id_prop ctxt variances (tyco, mapper);
-    val _ = Thm.cterm_of thy id_prop;
     val qualify = Binding.qualify true prfx o Binding.name;
+    fun mapper_declaration comp_thm id_thm phi context =
+      let
+        val typ_instance = Type.typ_instance (ProofContext.tsig_of (Context.proof_of context));
+        val mapper' = Morphism.term phi mapper;
+        val T_T' = pairself fastype_of (mapper, mapper');
+      in if typ_instance T_T' andalso typ_instance (swap T_T')
+        then Data.map (Symtab.update (tyco,
+          { mapper = mapper', variances = variances,
+            comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm })) context
+        else context
+      end;
     fun after_qed [single_comp_thm, single_id_thm] lthy =
       lthy
       |> Local_Theory.note ((qualify compN, []), single_comp_thm)
       ||>> Local_Theory.note ((qualify idN, []), single_id_thm)
       |-> (fn ((_, [comp_thm]), (_, [id_thm])) => fn lthy =>

             [prove_compositionality lthy comp_thm])
         |> snd
         |> Local_Theory.note ((qualify identityN, []),
             [prove_identity lthy id_thm])
         |> snd
-        |> Local_Theory.declaration false (fn phi => Data.map
-            (Symtab.update (tyco, { mapper = Morphism.term phi mapper, variances = variances,
-              comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm }))))
+        |> Local_Theory.declaration false (mapper_declaration comp_thm id_thm))
   in
     thy
     |> Named_Target.theory_init
     |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop])
   end