--- a/src/HOL/Tools/function_package/fundef_prep.ML Thu Dec 07 16:47:36 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_prep.ML Thu Dec 07 17:58:39 2006 +0100
@@ -508,8 +508,7 @@
PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
val lthy = PROFILE "abbrev"
- (LocalTheory.abbrevs ("", false) (* FIXME really this mode? cf. Syntax.default_mode *)
- [((defname ^ "_dom", NoSyn), mk_acc domT R)]) lthy
+ (TermSyntax.abbrevs Syntax.default_mode [((defname ^ "_dom", NoSyn), mk_acc domT R)]) lthy
val newthy = ProofContext.theory_of lthy
val clauses = map (transfer_clause_ctx newthy) clauses
--- a/src/Pure/Isar/specification.ML Thu Dec 07 16:47:36 2006 +0100
+++ b/src/Pure/Isar/specification.ML Thu Dec 07 17:58:39 2006 +0100
@@ -157,7 +157,7 @@
val mx = (case vars of [] => NoSyn | [((y, _), mx)] =>
if x = y then mx
else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
- val lthy2 = lthy1 |> LocalTheory.abbrevs mode [((x, mx), rhs)];
+ val lthy2 = lthy1 |> TermSyntax.abbrevs mode [((x, mx), rhs)];
in ((x, T), LocalTheory.restore lthy2) end;
val (cs, lthy') = lthy
@@ -174,7 +174,7 @@
(* notation *)
fun gen_notation prep_const mode args lthy =
- lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args);
+ lthy |> TermSyntax.notation mode (map (apfst (prep_const lthy)) args);
val notation = gen_notation ProofContext.read_const;
val notation_i = gen_notation (K I);
--- a/src/Pure/Isar/theory_target.ML Thu Dec 07 16:47:36 2006 +0100
+++ b/src/Pure/Isar/theory_target.ML Thu Dec 07 17:58:39 2006 +0100
@@ -72,7 +72,7 @@
val defs = abbrs |> map (fn (x, t) => (x, (("", []), t)));
in
lthy'
- |> is_loc ? LocalTheory.abbrevs Syntax.default_mode abbrs
+ |> is_loc ? TermSyntax.abbrevs Syntax.default_mode abbrs
|> LocalDefs.add_defs defs |>> map (apsnd snd)
end;