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/Nominal/nominal_fresh_fun.ML
changeset 55952 2f85cc6c27d4
parent 55951 c07d184aebe9
child 56230 3e449273942a 
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 06 12:10:19 2014 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 06 12:43:29 2014 +0100
@@ -185,7 +185,7 @@
      (Scan.succeed false);
 
 fun setup_generate_fresh x =
-  (Args.goal_spec -- Args.type_name {proper = false, strict = true} >>
+  (Args.goal_spec -- Args.type_name {proper = true, strict = true} >>
     (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
 
 fun setup_fresh_fun_simp x =
isabelle