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/datatype_realizer.ML
changeset 67399 eab6ce8368fa
parent 62922 96691631c1eb
child 67405 e9ab4ad7bd15 
--- a/src/HOL/Tools/datatype_realizer.ML	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Wed Jan 10 15:25:09 2018 +0100
@@ -34,7 +34,7 @@
       else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
 
     val rec_result_Ts = map (fn ((i, _), P) =>
-        if member (op =) is i then TFree ("'" ^ P, @{sort type}) else HOLogic.unitT)
+        if member (=) is i then TFree ("'" ^ P, @{sort type}) else HOLogic.unitT)
       (descr ~~ pnames);
 
     fun make_pred i T U r x =
isabelle