Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ctr_sugar_code.ML
changeset 54691 506312c293f5
parent 54615 62fb5af93fe2 
--- a/src/HOL/Tools/ctr_sugar_code.ML	Sat Dec 07 13:10:56 2013 +0100
+++ b/src/HOL/Tools/ctr_sugar_code.ML	Sat Dec 07 18:06:49 2013 +0100
@@ -110,8 +110,10 @@
     #> snd
   end;
 
-fun add_ctr_code fcT_name As ctrs inject_thms distinct_thms case_thms thy =
+fun add_ctr_code fcT_name raw_As raw_ctrs inject_thms distinct_thms case_thms thy =
   let
+    val As = map (perhaps (try Logic.unvarifyT_global)) raw_As;
+    val ctrs = map (apsnd (perhaps (try Logic.unvarifyT_global))) raw_ctrs;
     val fcT = Type (fcT_name, As);
     val unover_ctrs = map (fn ctr as (_, fcT) => (Axclass.unoverload_const thy ctr, fcT)) ctrs;
   in
isabelle