2007-04-15 wenzelm [Sun, 15 Apr 2007 23:25:50 +0200] rev 22709
removed obsolete TypeInfer.logicT -- use dummyT;
src/HOL/Import/proof_kernel.ML src/HOL/Nominal/nominal_primrec.ML src/HOL/Tools/datatype_package.ML src/HOL/Tools/specification_package.ML src/Pure/Isar/find_theorems.ML src/Pure/Syntax/mixfix.ML src/Pure/sign.ML src/Pure/simplifier.ML

2007-04-15 wenzelm [Sun, 15 Apr 2007 23:25:49 +0200] rev 22708
avoid internal names;
src/HOL/Bali/Example.thy

2007-04-15 wenzelm [Sun, 15 Apr 2007 14:32:55 +0200] rev 22707
tuned;
src/HOLCF/ROOT.ML

2007-04-15 wenzelm [Sun, 15 Apr 2007 14:32:07 +0200] rev 22706
legacy_infer_term/prop -- including intern_term;
src/HOLCF/domain/axioms.ML src/HOLCF/domain/library.ML src/HOLCF/domain/theorems.ML src/HOLCF/fixrec_package.ML

2007-04-15 wenzelm [Sun, 15 Apr 2007 14:32:05 +0200] rev 22705
Thm.plain_prop_of;
src/Pure/Tools/codegen_data.ML src/Pure/Tools/codegen_func.ML src/Pure/Tools/codegen_funcgr.ML src/Pure/Tools/compute.ML

2007-04-15 wenzelm [Sun, 15 Apr 2007 14:32:04 +0200] rev 22704
added decode_types (from type_infer.ML);
decode sorts: internalize here;
tuned;
src/Pure/Syntax/type_ext.ML

2007-04-15 wenzelm [Sun, 15 Apr 2007 14:32:03 +0200] rev 22703
added read_term;
adapted decoding of types/sorts;
src/Pure/Syntax/syntax.ML

2007-04-15 wenzelm [Sun, 15 Apr 2007 14:32:02 +0200] rev 22702
added mixfixT (from type_infer.ML);
src/Pure/Syntax/mixfix.ML

2007-04-15 wenzelm [Sun, 15 Apr 2007 14:32:01 +0200] rev 22701
proper interface infer_types(_pat);
Syntax.mixfixT;
tuned;
src/Pure/Isar/proof_context.ML

2007-04-15 wenzelm [Sun, 15 Apr 2007 14:32:00 +0200] rev 22700
Thm.fold_terms;
Syntax.mixfixT;
src/Pure/Isar/locale.ML