LocalTheory.abbrev;
authorwenzelm
Tue Dec 12 20:49:19 2006 +0100 (2006-12-12)
changeset 2179374409847e349
parent 21792 266a1056a2a3
child 21794 1a9f57f1bc3a
LocalTheory.abbrev;
src/HOL/Tools/function_package/fundef_prep.ML
src/HOL/Tools/inductive_package.ML
src/Pure/Isar/specification.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Tue Dec 12 17:29:26 2006 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Tue Dec 12 20:49:19 2006 +0100
     1.3 @@ -507,7 +507,7 @@
     1.4        val ((R, RIntro_thmss, R_elim), lthy) = 
     1.5            PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
     1.6  
     1.7 -      val lthy = PROFILE "abbrev"
     1.8 +      val (_, lthy) = PROFILE "abbrev"
     1.9          (LocalTheory.abbrev Syntax.default_mode ((defname ^ "_dom", NoSyn), mk_acc domT R)) lthy
    1.10  
    1.11        val newthy = ProofContext.theory_of lthy
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Dec 12 17:29:26 2006 +0100
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Dec 12 20:49:19 2006 +0100
     2.3 @@ -789,7 +789,7 @@
     2.4      ctxt |>
     2.5      add_ind_def verbose alt_name coind no_elim no_ind cs intros monos
     2.6        params cnames_syn'' ||>
     2.7 -    fold (LocalTheory.abbrev Syntax.default_mode) abbrevs''
     2.8 +    fold (snd oo LocalTheory.abbrev Syntax.default_mode) abbrevs''
     2.9    end;
    2.10  
    2.11  fun add_inductive verbose coind cnames_syn pnames_syn intro_srcs raw_monos ctxt =
     3.1 --- a/src/Pure/Isar/specification.ML	Tue Dec 12 17:29:26 2006 +0100
     3.2 +++ b/src/Pure/Isar/specification.ML	Tue Dec 12 20:49:19 2006 +0100
     3.3 @@ -153,7 +153,7 @@
     3.4        else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
     3.5      val lthy' = lthy
     3.6        |> ProofContext.set_syntax_mode mode    (* FIXME !? *)
     3.7 -      |> LocalTheory.abbrev mode ((x, mx), rhs)
     3.8 +      |> LocalTheory.abbrev mode ((x, mx), rhs) |> snd
     3.9        |> ProofContext.restore_syntax_mode lthy;
    3.10      val _ = print_consts lthy' (K false) [(x, T)]
    3.11    in lthy' end;