LocalTheory.notation/abbrev;
authorwenzelm
Sun Dec 10 15:30:45 2006 +0100 (2006-12-10)
changeset 217469d0652354513
parent 21745 a1d8806b5267
child 21747 d650305c609a
LocalTheory.notation/abbrev;
src/HOL/Tools/function_package/fundef_prep.ML
src/Pure/Isar/specification.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Sun Dec 10 15:30:44 2006 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Sun Dec 10 15:30:45 2006 +0100
     1.3 @@ -508,7 +508,7 @@
     1.4            PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
     1.5  
     1.6        val lthy = PROFILE "abbrev"
     1.7 -        (TermSyntax.abbrev Syntax.default_mode ((defname ^ "_dom", NoSyn), mk_acc domT R)) lthy
     1.8 +        (LocalTheory.abbrev Syntax.default_mode ((defname ^ "_dom", NoSyn), mk_acc domT R)) lthy
     1.9  
    1.10        val newthy = ProofContext.theory_of lthy
    1.11        val clauses = map (transfer_clause_ctx newthy) clauses
     2.1 --- a/src/Pure/Isar/specification.ML	Sun Dec 10 15:30:44 2006 +0100
     2.2 +++ b/src/Pure/Isar/specification.ML	Sun Dec 10 15:30:45 2006 +0100
     2.3 @@ -153,7 +153,7 @@
     2.4        else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
     2.5      val lthy' = lthy
     2.6        |> ProofContext.set_syntax_mode mode    (* FIXME !? *)
     2.7 -      |> TermSyntax.abbrev mode ((x, mx), rhs)
     2.8 +      |> LocalTheory.abbrev mode ((x, mx), rhs)
     2.9        |> ProofContext.restore_syntax_mode lthy;
    2.10      val _ = print_consts lthy' (K false) [(x, T)]
    2.11    in lthy' end;
    2.12 @@ -165,7 +165,7 @@
    2.13  (* notation *)
    2.14  
    2.15  fun gen_notation prep_const mode args lthy =
    2.16 -  lthy |> TermSyntax.notation mode (map (apfst (prep_const lthy)) args);
    2.17 +  lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args);
    2.18  
    2.19  val notation = gen_notation ProofContext.read_const;
    2.20  val notation_i = gen_notation (K I);