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_inductive2.ML
changeset 30763 6976521b4263
parent 30450 7655e6533209
child 31174 f1f1e9b53c81 
--- a/src/HOL/Nominal/nominal_inductive2.ML	Sat Mar 28 17:21:49 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat Mar 28 17:53:33 2009 +0100
@@ -181,7 +181,7 @@
       | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs));
     fun mk_avoids params name sets =
       let
-        val (_, ctxt') = ProofContext.add_fixes_i
+        val (_, ctxt') = ProofContext.add_fixes
           (map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) ctxt;
         fun mk s =
           let
isabelle